1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
  5  -/
  6  
  7  import algebra.ring
src         └──────────┘
  8  import data.finsupp data.polynomial data.equiv.algebra
src         └──────────┘ └─────────────┘ └────────────────┘
  9  
 10  /-!
 11  # Multivariate polynomials
 12  
 13  This file defines polynomial rings over a base ring (or even semiring),
 14  with variables from a general type `σ` (which could be infinite).
 15  
 16  ## Important definitions
 17  
 18  Let `R` be a commutative ring (or a semiring) and let `σ` be an arbitrary
 19  type. This file creates the type `mv_polynomial σ R`, which mathematicians
 20  might denote `R[X_i : i ∈ σ]`. It is the type of multivariate
 21  (a.k.a. multivariable) polynomials, with variables
 22  corresponding to the terms in `σ`, and coefficients in `R`.
 23  
 24  ### Notation
 25  
 26  In the definitions below, we use the following notation:
 27  
 28  + `σ : Type*` (indexing the variables)
 29  
 30  + `R : Type*` `[comm_semiring R]` (the coefficients)
 31  
 32  + `s : σ →₀ ℕ`, a function from `σ` to `ℕ` which is zero away from a finite set.
 33  This will give rise to a monomial in `mv_polynomial σ R` which mathematicians might call `X^s`
 34  
 35  + `a : R`
 36  
 37  + `i : σ`, with corresponding monomial `X i`, often denoted `X_i` by mathematicians
 38  
 39  + `p : mv_polynomial σ R`
 40  
 41  ### Definitions
 42  
 43  * `mv_polynomial σ R` : the type of polynomials with variables of type `σ` and coefficients
 44    in the commutative semiring `R`
 45  
 46  * `monomial s a` : the monomial which mathematically would be denoted `a * X^s`
 47  
 48  * `C a` : the constant polynomial with value `a`
 49  
 50  * `X i` : the degree one monomial corresponding to i; mathematically this might be denoted `Xᵢ`.
 51  
 52  * `coeff s p` : the coefficient of `s` in `p`.
 53  
 54  * `eval₂ (f : R → S) (g : σ → S) p` : given a semiring homomorphism from `R` to another
 55    semiring `S`, and a map `σ → S`, evaluates `p` at this valuation, returning a term of type `S`.
 56    Note that `eval₂` can be made using `eval` and `map` (see below), and it has been suggested
 57    that sticking to `eval` and `map` might make the code less brittle.
 58  
 59  * `eval (g : σ → R) p` : given a map `σ → R`, evaluates `p` at this valuation,
 60    returning a term of type `R`
 61  
 62  * `map (f : R → S) p` : returns the multivariate polynomial obtained from `p` by the change of
 63    coefficient semiring corresponding to `f`
 64  
 65  * `degrees p` : the multiset of variables representing the union of the multisets corresponding
 66    to each non-zero monomial in `p`. For example if `7 ≠ 0` in `R` and `p = x²y+7y³` then
 67    `degrees p = {x, x, y, y, y}`
 68  
 69  * `vars p` : the finset of variables occurring in `p`. For example if `p = x⁴y+yz` then
 70    `vars p = {x, y, z}`
 71  
 72  * `degree_of n p : ℕ` -- the total degree of `p` with respect to the variable `n`. For example
 73    if `p = x⁴y+yz` then `degree_of y p = 1`.
 74  
 75  * `total_degree p : ℕ` -- the max of the sizes of the multisets `s` whose monomials `X^s` occur
 76    in `p`. For example if `p = x⁴y+yz` then `total_degree p = 5`.
 77  
 78  ## Implementation notes
 79  
 80  Recall that if `Y` has a zero, then `X →₀ Y` is the type of functions from `X` to `Y` with finite
 81  support, i.e. such that only finitely many elements of `X` get sent to non-zero terms in `Y`.
 82  The definition of `mv_polynomial σ α` is `(σ →₀ ℕ) →₀ α` ; here `σ →₀ ℕ` denotes the space of all
 83  monomials in the variables, and the function to α sends a monomial to its coefficient in
 84  the polynomial being represented.
 85  
 86  ## Tags
 87  
 88  polynomial, multivariate polynomial, multivariable polynomial
 89  -/
 90  
 91  noncomputable theory
 92  local attribute [instance, priority 100] classical.prop_decidable
id                                            └──────────────────────┘
src                                           └──────────────────────┘
typ                                           └──────────────────────┘
 93  
 94  open set function finsupp lattice
 95  
 96  universes u v w x
 97  variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 98  
 99  /-- Multivariate polynomial, where `σ` is the index set of the variables and
100    `α` is the coefficient ring -/
101  def mv_polynomial (σ : Type*) (α : Type*) [comm_semiring α] := (σ →₀ ℕ) →₀ α
id                                              └───────────┘        └┘   └┘ 
src                                             └───────────┘          └┘   └┘
typ                                             └───────────┘        └┘   └┘ 
doc                                                                    └┘    └┘
102  
103  namespace mv_polynomial
104  variables {σ : Type*} {a a' a₁ a₂ : α} {e : ℕ} {n m : σ} {s : σ →₀ ℕ}
id                                                                  └┘ 
src                                                                 └┘ 
typ                                                                 └┘ 
doc                                                                  └┘
st                                  └┘
105  
106  section comm_semiring
107  variables [comm_semiring α] {p q : mv_polynomial σ α}
id              └───────────┘           └───────────┘
src             └───────────┘           └───────────┘
typ             └───────────┘           └───────────┘
doc                                     └───────────┘
108  
109  instance decidable_eq_mv_polynomial [decidable_eq σ] [decidable_eq α] :
id                                        └──────────┘    └──────────┘ 
src                                       └──────────┘     └──────────┘
typ                                       └──────────┘    └──────────┘ 
110    decidable_eq (mv_polynomial σ α) := finsupp.decidable_eq
id     └──────────┘  └───────────┘       └──────────────────┘
src    └──────────┘  └───────────┘         └──────────────────┘
typ    └──────────┘  └───────────┘       └──────────────────┘
doc                  └───────────┘
111  instance : has_zero (mv_polynomial σ α) := finsupp.has_zero
id              └──────┘  └───────────┘       └──────────────┘
src             └──────┘  └───────────┘         └──────────────┘
typ             └──────┘  └───────────┘       └──────────────┘
doc                       └───────────┘
112  instance : has_one (mv_polynomial σ α) := finsupp.has_one
id              └─────┘  └───────────┘       └─────────────┘
src             └─────┘  └───────────┘         └─────────────┘
typ             └─────┘  └───────────┘       └─────────────┘
doc                      └───────────┘         └─────────────┘
113  instance : has_add (mv_polynomial σ α) := finsupp.has_add
id              └─────┘  └───────────┘       └─────────────┘
src             └─────┘  └───────────┘         └─────────────┘
typ             └─────┘  └───────────┘       └─────────────┘
doc                      └───────────┘
114  instance : has_mul (mv_polynomial σ α) := finsupp.has_mul
id              └─────┘  └───────────┘       └─────────────┘
src             └─────┘  └───────────┘         └─────────────┘
typ             └─────┘  └───────────┘       └─────────────┘
doc                      └───────────┘         └─────────────┘
115  instance : comm_semiring (mv_polynomial σ α) := finsupp.comm_semiring
id              └───────────┘  └───────────┘       └───────────────────┘
src             └───────────┘  └───────────┘         └───────────────────┘
typ             └───────────┘  └───────────┘       └───────────────────┘
doc                            └───────────┘
116  instance : inhabited (mv_polynomial σ α) := ⟨0⟩
id              └───────┘  └───────────┘  
src             └───────┘  └───────────┘
typ             └───────┘  └───────────┘  
doc                        └───────────┘
117  
118  /-- `monomial s a` is the monomial `a * X^s` -/
119  def monomial (s : σ →₀ ℕ) (a : α) : mv_polynomial σ α := single s a
id                      └┘            └───────────┘      └────┘  
src                      └┘             └───────────┘        └────┘
typ                     └┘            └───────────┘      └────┘  
doc                      └┘              └───────────┘        └────┘
120  
121  /-- `C a` is the constant polynomial with value `a` -/
122  def C (a : α) : mv_polynomial σ α := monomial 0 a
id                  └───────────┘      └──────┘   
src                  └───────────┘        └──────┘
typ                 └───────────┘      └──────┘   
doc                  └───────────┘        └──────┘
123  
124  /-- `X n` is the degree `1` monomial `1*n` -/
125  def X (n : σ) : mv_polynomial σ α := monomial (single n 1) 1
id                  └───────────┘      └──────┘  └────┘ 
src                  └───────────┘        └──────┘  └────┘
typ                 └───────────┘      └──────┘  └────┘ 
doc                  └───────────┘        └──────┘  └────┘
126  
127  @[simp] lemma C_0 : C 0 = (0 : mv_polynomial σ α) := by simp [C, monomial]; refl
id                                └───────────┘                  └──────┘
src                               └───────────┘            └────┘└┘└──────┘  └────
typ                               └───────────┘          └────┘└┘└──────┘  └────
doc    └──┘                        └───────────┘            └────┘└┘└──────┘  └────
txt                                                          └────┘ └┘          └────
par                                                          └────┘ └┘          └────
pid                                                               └┘              
st                                                          └─────────────────────────
128  
src  
typ  
doc  
txt  
par  
pid  
st   
129  @[simp] lemma C_1 : C 1 = (1 : mv_polynomial σ α) := rfl
id                                └───────────┘       └─┘
src                               └───────────┘         └─┘
typ                               └───────────┘       └─┘
doc    └──┘                        └───────────┘
130  
131  lemma C_mul_monomial : C a * monomial s a' = monomial s (a * a') :=
id                             └──────┘  └┘  └──────┘     └┘
src                             └──────┘       └──────┘      
typ                            └──────┘  └┘  └──────┘     └┘
doc                              └──────┘        └──────┘
132  by simp [C, monomial, single_mul_single]
id              └──────┘  └───────────────┘
src     └────┘└┘└──────┘└┘└───────────────┘└─
typ     └────┘└┘└──────┘└┘└───────────────┘└─
doc     └────┘└┘└──────┘└┘                 └─
txt     └────┘ └┘        └┘                 └─
par     └────┘ └┘        └┘                 └─
pid          └┘        └┘                 
st     └──────────────────────────────────────
133  
src  
typ  
doc  
txt  
par  
pid  
st   
134  @[simp] lemma C_add : (C (a + a') : mv_polynomial σ α) = C a + C a' := single_add
id                              └┘    └───────────┘         └┘    └────────┘
src                                    └───────────┘                  └────────┘
typ                             └┘    └───────────┘         └┘    └────────┘
doc    └──┘                             └───────────┘             
135  
136  @[simp] lemma C_mul : (C (a * a') : mv_polynomial σ α) = C a * C a' := C_mul_monomial.symm
id                              └┘    └───────────┘         └┘    └────────────┘└───┘
src                                    └───────────┘                  └────────────┘└───┘
typ                             └┘    └───────────┘         └┘    └────────────┘└───┘
doc    └──┘                             └───────────┘             
137  
138  @[simp] lemma C_pow (a : α) (n : ℕ) : (C (a^n) : mv_polynomial σ α) = (C a)^n :=
id                                              └───────────┘        
src                                                └───────────┘           
typ                                             └───────────┘        
doc    └──┘                                          └───────────┘         
139  by induction n; simp [pow_succ, *]
id                        └──────┘
src     └────────┘   └────┘└──────┘└────
typ     └────────┘  └────┘└──────┘└────
doc     └────────┘   └────┘        └────
txt     └────────┘   └────┘        └────
par     └────────┘   └────┘        └────
pid                             └──┘
st     └────────────────────────────────
140  
src  
typ  
doc  
txt  
par  
pid  
st   
141  instance : is_semiring_hom (C : α → mv_polynomial σ α) :=
id              └─────────────┘        └───────────┘  
src             └─────────────┘         └───────────┘
typ             └─────────────┘        └───────────┘  
doc             └─────────────┘         └───────────┘
142  { map_zero := C_0,
id                 └─┘
src                └─┘
typ                └─┘
143    map_one := C_1,
id                └─┘
src               └─┘
typ               └─┘
144    map_add := λ a a', C_add,
id                   └┘  └───┘
src                       └───┘
typ                  └┘  └───┘
145    map_mul := λ a a', C_mul }
id                   └┘  └───┘
src                       └───┘
typ                  └┘  └───┘
146  
147  lemma C_eq_coe_nat (n : ℕ) : (C ↑n : mv_polynomial σ α) = n :=
id                                    └───────────┘     
src                                    └───────────┘      
typ                                   └───────────┘     
doc                                      └───────────┘
148  by induction n; simp [nat.succ_eq_add_one, *]
id                        └─────────────────┘
src     └────────┘   └────┘└─────────────────┘└────
typ     └────────┘  └────┘└─────────────────┘└────
doc     └────────┘   └────┘                   └────
txt     └────────┘   └────┘                   └────
par     └────────┘   └────┘                   └────
pid                                        └──┘
st     └───────────────────────────────────────────
149  
src  
typ  
doc  
txt  
par  
pid  
st   
150  lemma X_pow_eq_single : X n ^ e = monomial (single n e) (1 : α) :=
id                                └──────┘  └────┘         
src                                 └──────┘  └────┘
typ                               └──────┘  └────┘         
doc                                   └──────┘  └────┘
151  begin
st   └─────
152    induction e,
id               
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ────────────┘└─
153    { simp [X], refl },
id             
src      └────┘  └───┘
typ      └────┘  └───┘
doc      └────┘  └───┘
txt      └────┘   └───┘
par      └────┘   └───┘
pid                 
st   ───┘└──────┘└─────┘└┘
154    { simp [pow_succ, e_ih],
id             └──────┘  └──┘
src      └────┘└──────┘└┘    
typ      └────┘└──────┘└┘└──┘
doc      └────┘        └┘    
txt      └────┘        └┘    
par      └────┘        └┘    
pid                  └┘    
st   ────────────────────────┘└─
155      simp [X, monomial, single_mul_single, nat.succ_eq_add_one] }
id               └──────┘  └───────────────┘  └─────────────────┘
src      └────┘└┘└──────┘└┘└───────────────┘└┘└─────────────────┘└┘
typ      └────┘└┘└──────┘└┘└───────────────┘└┘└─────────────────┘└┘
doc      └────┘└┘└──────┘└┘                 └┘                   └┘
txt      └────┘ └┘        └┘                 └┘                   └┘
par      └────┘ └┘        └┘                 └┘                   └┘
pid           └┘        └┘                 └┘                   
st   ──────────────────────────────────────────────────────────────┘└─
156  end
st   ──┘
157  
158  lemma monomial_add_single : monomial (s + single n e) a = (monomial s a * X n ^ e) :=
id                               └──────┘    └────┘       └──────┘       
src                              └──────┘     └────┘          └──────┘         
typ                              └──────┘    └────┘       └──────┘       
doc                              └──────┘      └────┘           └──────┘       
159  by rw [X_pow_eq_single, monomial, monomial, monomial, single_mul_single]; simp
id          └─────────────┘  └──────┘  └──────┘  └──────┘  └───────────────┘
src     └──┘└─────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────────────┘  └────
typ     └──┘└─────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────────────┘  └────
doc     └──┘               └┘└──────┘└┘└──────┘└┘└──────┘└┘                   └────
txt     └──┘               └┘        └┘        └┘        └┘                   └────
par     └──┘               └┘        └┘        └┘        └┘                   └────
pid       └┘               └┘        └┘        └┘        └┘                       
st     └──────────────────┘└────────┘└────────┘└────────┘└─────────────────┘└──────
160  
src  
typ  
doc  
txt  
par  
pid  
st   
161  lemma monomial_single_add : monomial (single n e + s) a = (X n ^ e * monomial s a) :=
id                               └──────┘  └────┘              └──────┘  
src                              └──────┘  └────┘                    └──────┘
typ                              └──────┘  └────┘              └──────┘  
doc                              └──────┘  └────┘                        └──────┘
162  by rw [X_pow_eq_single, monomial, monomial, monomial, single_mul_single]; simp
id          └─────────────┘  └──────┘  └──────┘  └──────┘  └───────────────┘
src     └──┘└─────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────────────┘  └────
typ     └──┘└─────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└───────────────┘  └────
doc     └──┘               └┘└──────┘└┘└──────┘└┘└──────┘└┘                   └────
txt     └──┘               └┘        └┘        └┘        └┘                   └────
par     └──┘               └┘        └┘        └┘        └┘                   └────
pid       └┘               └┘        └┘        └┘        └┘                       
st     └──────────────────┘└────────┘└────────┘└────────┘└─────────────────┘└──────
163  
src  
typ  
doc  
txt  
par  
pid  
st   
164  lemma monomial_eq : monomial s a = C a * (s.prod $ λn e, X n ^ e : mv_polynomial σ α) :=
id                       └──────┘        └───┘             └───────────┘  
src                      └──────┘            └───┘                 └───────────┘
typ                      └──────┘        └───┘             └───────────┘  
doc                      └──────┘              └───┘                  └───────────┘
165  begin
st   └─────
166    apply @finsupp.induction σ ℕ _ _ s,
id            └───────────────┘        
src    └────┘ └───────────────┘  └───┘
typ    └────┘ └───────────────┘ └───┘
doc    └────┘                    └───┘
txt    └────┘                    └───┘
par    └────┘                    └───┘
pid                             └───┘
st   ───────────────────────────────────┘└─
167    { simp [C, prod_zero_index]; exact (mul_one _).symm },
id               └─────────────┘
src      └────┘└┘└─────────────┘  └────┘        └───────┘
typ      └────┘└┘└─────────────┘  └────┘        └───────┘
doc      └────┘└┘                 └────┘        └───────┘
txt      └────┘ └┘                 └────┘        └───────┘
par      └────┘ └┘                 └────┘        └───────┘
pid           └┘                              └─────┘└┘
st   ───┘└────────────────────────────────────────────────┘└┘
168    { assume n e s hns he ih,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid      └────────────────────┘
st   ─────────────────────────┘└─
169      simp [prod_add_index, prod_single_index, pow_zero, pow_add, (mul_assoc _ _ _).symm, ih.symm,
id             └────────────┘  └───────────────┘  └──────┘  └─────┘   └───────┘
src      └────┘└────────────┘└┘└───────────────┘└┘└──────┘└┘└─────┘└┘ └───────┘└────────────┘       └─
typ      └────┘└────────────┘└┘└───────────────┘└┘└──────┘└┘└─────┘└┘ └───────┘└────────────┘└─────┘└─
doc      └────┘              └┘                 └┘        └┘       └┘          └────────────┘       └─
txt      └────┘              └┘                 └┘        └┘       └┘          └────────────┘       └─
par      └────┘              └┘                 └┘        └┘       └┘          └────────────┘       └─
pid                        └┘                 └┘        └┘       └┘          └────────────┘       └─
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
170        monomial_add_single] }
id         └─────────────────┘
src  ─────┘└─────────────────┘└┘
typ  ─────┘└─────────────────┘└┘
doc  ─────┘                   └┘
txt  ─────┘                   └┘
par  ─────┘                   └┘
pid  ─────┘                   
st   ──────────────────────────┘└─
171  end
st   ──┘
172  
173  @[recursor 5]
doc    └──────┘
174  lemma induction_on {M : mv_polynomial σ α → Prop} (p : mv_polynomial σ α)
id                           └───────────┘                └───────────┘  
src                          └───────────┘                  └───────────┘
typ                          └───────────┘                └───────────┘  
doc                          └───────────┘                  └───────────┘
175    (h_C : ∀a, M (C a)) (h_add : ∀p q, M p → M q → M (p + q)) (h_X : ∀p n, M p → M (p * X n)) :
id                                                                     
src                                                                                     
typ                                                                    
doc                                                                                       
176    M p :=
id      
typ     
177  have ∀s a, M (monomial s a),
id              └──────┘  
src                └──────┘
typ             └──────┘  
doc                └──────┘
178  begin
st   └─────
179    assume s a,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid    └────────┘
st   ───────────┘└─
180    apply @finsupp.induction σ ℕ _ _ s,
id            └───────────────┘        
src    └────┘ └───────────────┘  └───┘
typ    └────┘ └───────────────┘ └───┘
doc    └────┘                    └───┘
txt    └────┘                    └───┘
par    └────┘                    └───┘
pid                             └───┘
st   ───────────────────────────────────┘└─
181    { show M (monomial 0 a), from h_C a, },
id              └──────┘           └─┘ 
src      └───┘  └──────┘└─┘   └───┘   
typ      └───┘ └──────┘└─┘  └───┘└─┘
doc      └───┘  └──────┘└─┘   └───┘   
txt      └───┘          └─┘   └───┘   
par      └───┘          └─┘   └───┘   
pid      └───┘          └─┘   └───┘   
st   ───┘└───────────────────┘└──────────┘└──┘
182    { assume n e p hpn he ih,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid      └────────────────────┘
st   ─────────────────────────┘└─
183      have : ∀e:ℕ, M (monomial p a * X n ^ e),
id                      └──────┘      
src      └─────┘ └┘    └──────┘    
typ      └─────┘ └┘   └──────┘ 
doc      └─────┘ └┘    └──────┘      
txt      └─────┘ └┘                   
par      └─────┘ └┘                   
pid      └───┘└┘ └┘                   
st   ──────────────────────────────────────────┘└─
184      { intro e,
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid             └┘
st   ─────┘└─────┘└─
185        induction e,
id                   
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid                 
st   ────────────────┘└─
186        { simp [ih] },
id                 └┘
src          └────┘  └┘
typ          └────┘└┘└┘
doc          └────┘  └┘
txt          └────┘  └┘
par          └────┘  └┘
pid                
st   ───────┘└────────┘└┘
187        { simp [ih, pow_succ', (mul_assoc _ _ _).symm, h_X, e_ih] } },
id                 └┘  └───────┘   └───────┘              └─┘  └──┘
src          └────┘  └┘└───────┘└┘ └───────┘└────────────┘   └┘    └┘
typ          └────┘└┘└┘└───────┘└┘ └───────┘└────────────┘└─┘└┘└──┘└┘
doc          └────┘  └┘         └┘          └────────────┘   └┘    └┘
txt          └────┘  └┘         └┘          └────────────┘   └┘    └┘
par          └────┘  └┘         └┘          └────────────┘   └┘    └┘
pid                └┘         └┘          └────────────┘   └┘    
st   ───────────────────────────────────────────────────────────────┘└──┘
188      simp [monomial_add_single, this] }
id             └─────────────────┘  └──┘
src      └────┘└─────────────────┘└┘    └┘
typ      └────┘└─────────────────┘└┘└──┘└┘
doc      └────┘                   └┘    └┘
txt      └────┘                   └┘    └┘
par      └────┘                   └┘    └┘
pid                             └┘    
st   ────────────────────────────────────┘└─
189  end,
st   ──┘
190  finsupp.induction p
id   └───────────────┘ 
src  └───────────────┘
typ  └───────────────┘ 
191    (by have : M (C 0) := h_C 0; rwa [C_0] at this)
id                         └─┘         └─┘
src        └─────┘  └─────┘   └┘  └───┘└─┘└───────┘
typ        └─────┘ └─────┘└─┘└┘  └───┘└─┘└───────┘
doc        └─────┘  └─────┘   └┘  └───┘   └───────┘
txt        └─────┘   └─────┘   └┘  └───┘   └───────┘
par        └─────┘   └─────┘   └┘  └───┘   └───────┘
pid        └───┘└┘   └─┘└──┘        └┘   └──────┘
st        └─────────────────────────────┘└─┘└──────┘
192    (assume s a p hsp ha hp, h_add _ _ (this s a) hp)
id                └─┘ └┘ └┘  └───┘      └──┘    └┘
typ               └─┘ └┘ └┘  └───┘      └──┘    └┘
193  
194  lemma hom_eq_hom [semiring γ]
id                     └──────┘ 
src                    └──────┘
typ                    └──────┘ 
195    (f g : mv_polynomial σ α → γ) (hf : is_semiring_hom f) (hg : is_semiring_hom g)
id            └───────────┘             └─────────────┘         └─────────────┘ 
src           └───────────┘                └─────────────┘          └─────────────┘
typ           └───────────┘             └─────────────┘         └─────────────┘ 
doc           └───────────┘                └─────────────┘          └─────────────┘
196    (hC : ∀a:α, f (C a) = g (C a)) (hX : ∀n:σ, f (X n) = g (X n)) (p : mv_polynomial σ α) :
id                                                        └───────────┘  
src                                                                 └───────────┘
typ                                                       └───────────┘  
doc                                                                   └───────────┘
197    f p = g p :=
id         
src        
typ        
198  mv_polynomial.induction_on p hC
id   └────────────────────────┘  └┘
src  └────────────────────────┘
typ  └────────────────────────┘  └┘
199    begin assume p q hp hq, rw [is_semiring_hom.map_add f, is_semiring_hom.map_add g, hp, hq] end
id                                 └─────────────────────┘   └─────────────────────┘   └┘  └┘
src          └──────────────┘  └──┘└─────────────────────┘ └┘└─────────────────────┘ └┘  └┘  └┘
typ          └──────────────┘  └──┘└─────────────────────┘└┘└─────────────────────┘└┘└┘└┘└┘└┘
doc          └──────────────┘  └──┘                        └┘                        └┘  └┘  └┘
txt          └──────────────┘  └──┘                        └┘                        └┘  └┘  └┘
par          └──────────────┘  └──┘                        └┘                        └┘  └┘  └┘
pid          └──────────────┘    └┘                        └┘                        └┘  └┘  
st     └────────────────────┘└─────────────────────────────┘└─────────────────────────┘└──┘└──┘└─┘
200    begin assume p n hp, rw [is_semiring_hom.map_mul f, is_semiring_hom.map_mul g, hp, hX] end
id                              └─────────────────────┘   └─────────────────────┘   └┘  └┘
src          └───────────┘  └──┘└─────────────────────┘ └┘└─────────────────────┘ └┘  └┘  └┘
typ          └───────────┘  └──┘└─────────────────────┘└┘└─────────────────────┘└┘└┘└┘└┘└┘
doc          └───────────┘  └──┘                        └┘                        └┘  └┘  └┘
txt          └───────────┘  └──┘                        └┘                        └┘  └┘  └┘
par          └───────────┘  └──┘                        └┘                        └┘  └┘  └┘
pid          └───────────┘    └┘                        └┘                        └┘  └┘  
st     └─────────────────┘└─────────────────────────────┘└─────────────────────────┘└──┘└──┘└─┘
201  
202  lemma is_id (f : mv_polynomial σ α → mv_polynomial σ α) (hf : is_semiring_hom f)
id                    └───────────┘     └───────────┘          └─────────────┘ 
src                   └───────────┘       └───────────┘            └─────────────┘
typ                   └───────────┘     └───────────┘          └─────────────┘ 
doc                   └───────────┘       └───────────┘            └─────────────┘
203    (hC : ∀a:α, f (C a) = (C a)) (hX : ∀n:σ, f (X n) = (X n)) (p : mv_polynomial σ α) :
id                                                      └───────────┘  
src                                                             └───────────┘
typ                                                     └───────────┘  
doc                                                               └───────────┘
204    f p = p :=
id        
src        
typ       
205  hom_eq_hom f id hf is_semiring_hom.id hC hX p
id   └────────┘  └┘ └┘ └────────────────┘ └┘ └┘ 
src  └────────┘   └┘    └────────────────┘
typ  └────────┘  └┘ └┘ └────────────────┘ └┘ └┘ 
doc                     └────────────────┘
206  
207  section coeff
208  
209  section
210  -- While setting up `coeff`, we make `mv_polynomial` reducible so we can treat it as a function.
211  local attribute [reducible] mv_polynomial
id                               └───────────┘
src                              └───────────┘
typ                              └───────────┘
doc                   └───────┘  └───────────┘
212  
213  /-- The coefficient of the monomial `m` in the multi-variable polynomial `p`. -/
214  def coeff (m : σ →₀ ℕ) (p : mv_polynomial σ α) : α := p m
id                   └┘        └───────────┘           
src                   └┘        └───────────┘
typ                  └┘        └───────────┘           
doc                   └┘         └───────────┘
215  end
216  
217  lemma ext (p q : mv_polynomial σ α) :
id                    └───────────┘  
src                   └───────────┘
typ                   └───────────┘  
doc                   └───────────┘
218    (∀ m, coeff m p = coeff m q) → p = q := ext
id          └───┘    └───┘            └─┘
src          └───┘      └───┘                └─┘
typ         └───┘    └───┘            └─┘
doc          └───┘       └───┘
219  
220  lemma ext_iff (p q : mv_polynomial σ α) :
id                        └───────────┘  
src                       └───────────┘
typ                       └───────────┘  
doc                       └───────────┘
221    (∀ m, coeff m p = coeff m q) ↔ p = q :=
id          └───┘    └───┘       
src          └───┘      └───┘         
typ         └───┘    └───┘       
doc          └───┘       └───┘
222  ⟨ext p q, λ h m, by rw h⟩
id    └─┘               
src   └─┘                └─┘
typ   └─┘            └─┘
doc                      └─┘
txt                      └─┘
par                      └─┘
pid                        
st                      └───┘
223  
224  @[simp] lemma coeff_add (m : σ →₀ ℕ) (p q : mv_polynomial σ α) :
id                                 └┘          └───────────┘  
src                                 └┘          └───────────┘
typ                                └┘          └───────────┘  
doc    └──┘                         └┘           └───────────┘
225    coeff m (p + q) = coeff m p + coeff m q := add_apply
id     └───┘        └───┘    └───┘      └───────┘
src    └───┘           └───┘      └───┘        └───────┘
typ    └───┘        └───┘    └───┘      └───────┘
doc    └───┘             └───┘       └───┘
226  
227  @[simp] lemma coeff_zero (m : σ →₀ ℕ) :
id                                  └┘ 
src                                  └┘ 
typ                                 └┘ 
doc    └──┘                          └┘
228    coeff m (0 : mv_polynomial σ α) = 0 := rfl
id     └───┘       └───────────┘          └─┘
src    └───┘        └───────────┘            └─┘
typ    └───┘       └───────────┘          └─┘
doc    └───┘        └───────────┘
229  
230  @[simp] lemma coeff_zero_X (i : σ) : coeff 0 (X i : mv_polynomial σ α) = 0 :=
id                                       └───┘        └───────────┘    
src                                       └───┘         └───────────┘      
typ                                      └───┘        └───────────┘    
doc    └──┘                               └───┘         └───────────┘
231  single_eq_of_ne (λ h, by cases single_eq_zero.1 h)
id   └─────────────┘               └────────────┘   
src  └─────────────┘          └────┘└────────────┘└─┘
typ  └─────────────┘         └────┘└────────────┘└─┘
doc                           └────┘              └─┘
txt                           └────┘              └─┘
par                           └────┘              └─┘
pid                                              └─┘
st                           └───────────────────────┘
232  
233  instance coeff.is_add_monoid_hom (m : σ →₀ ℕ) :
id                                          └┘ 
src                                          └┘ 
typ                                         └┘ 
doc                                          └┘
234    is_add_monoid_hom (coeff m : mv_polynomial σ α → α) :=
id     └───────────────┘  └───┘    └───────────┘     
src    └───────────────┘  └───┘     └───────────┘
typ    └───────────────┘  └───┘    └───────────┘     
doc    └───────────────┘  └───┘     └───────────┘
235  { map_add := coeff_add m,
id                └───────┘ 
src               └───────┘
typ               └───────┘ 
236    map_zero := coeff_zero m }
id                 └────────┘ 
src                └────────┘
typ                └────────┘ 
237  
238  lemma coeff_sum {X : Type*} (s : finset X) (f : X → mv_polynomial σ α) (m : σ →₀ ℕ) :
id                                    └────┘           └───────────┘          └┘ 
src                                   └────┘             └───────────┘             └┘ 
typ                                   └────┘           └───────────┘          └┘ 
doc                                   └────┘             └───────────┘             └┘
239    coeff m (s.sum f) = s.sum (λ x, coeff m (f x)) :=
id     └───┘   └──┘    └──┘      └───┘    
src    └───┘     └──┘      └──┘       └───┘
typ    └───┘   └──┘    └──┘      └───┘    
doc    └───┘                           └───┘
240  (s.sum_hom _).symm
id    └──────┘   └──┘
src    └──────┘   └──┘
typ   └──────┘   └──┘
241  
242  lemma monic_monomial_eq (m) : monomial m (1:α) = (m.prod $ λn e, X n ^ e : mv_polynomial σ α) :=
id                                 └──────┘         └───┘             └───────────┘  
src                                └──────┘            └───┘                 └───────────┘
typ                                └──────┘         └───┘             └───────────┘  
doc                                └──────┘             └───┘                  └───────────┘
243  by simp [monomial_eq]
id            └─────────┘
src     └────┘└─────────┘└─
typ     └────┘└─────────┘└─
doc     └────┘           └─
txt     └────┘           └─
par     └────┘           └─
pid                    
st     └───────────────────
244  
src  
typ  
doc  
txt  
par  
pid  
st   
245  @[simp] lemma coeff_monomial (m n) (a) :
doc    └──┘
246    coeff m (monomial n a : mv_polynomial σ α) = if n = m then a else 0 :=
id     └───┘   └──────┘     └───────────┘                
src    └───┘    └──────┘       └───────────┘            
typ    └───┘   └──────┘     └───────────┘                
doc    └───┘    └──────┘       └───────────┘
247  by convert single_apply
id              └──────────┘
src     └──────┘└──────────┘
typ     └──────┘└──────────┘
doc     └──────┘            
txt     └──────┘            
par     └──────┘            
pid                        
st     └─────────────────────
248  
src  
typ  
doc  
txt  
par  
pid  
st   
249  @[simp] lemma coeff_C (m) (a) :
doc    └──┘
250    coeff m (C a : mv_polynomial σ α) = if 0 = m then a else 0 :=
id     └───┘       └───────────┘                 
src    └───┘         └───────────┘            
typ    └───┘       └───────────┘                 
doc    └───┘         └───────────┘
251  by convert single_apply
id              └──────────┘
src     └──────┘└──────────┘
typ     └──────┘└──────────┘
doc     └──────┘            
txt     └──────┘            
par     └──────┘            
pid                        
st     └─────────────────────
252  
src  
typ  
doc  
txt  
par  
pid  
st   
253  lemma coeff_X_pow (i : σ) (m) (k : ℕ) :
id                                     
src                                     
typ                                    
254    coeff m (X i ^ k : mv_polynomial σ α) = if single i k = m then 1 else 0 :=
id     └───┘         └───────────┘        └────┘    
src    └───┘            └───────────┘          └────┘     
typ    └───┘         └───────────┘        └────┘    
doc    └───┘             └───────────┘           └────┘
255  begin
st   └─────
256    have := coeff_monomial m (finsupp.single i k) (1:α),
id             └────────────┘   └────────────┘       
src    └──────┘└────────────┘  └────────────┘  └┘ └┘ 
typ    └──────┘└────────────┘ └────────────┘└┘ └┘
doc    └──────┘                └────────────┘  └┘ └┘ 
txt    └──────┘                                └┘ └┘ 
par    └──────┘                                └┘ └┘ 
pid    └───┘└─┘                                └┘ └┘ 
st   ────────────────────────────────────────────────────┘└─
257    rwa [@monomial_eq _ _ (1:α) (finsupp.single i k) _,
id           └─────────┘           └────────────┘  
src    └───┘ └─────────┘└───┘ └┘ └┘ └────────────┘  └────
typ    └───┘ └─────────┘└───┘ └┘└┘ └────────────┘└────
doc    └───┘            └───┘ └┘ └┘ └────────────┘  └────
txt    └───┘            └───┘ └┘ └┘                 └────
par    └───┘            └───┘ └┘ └┘                 └────
pid       └┘            └───┘ └┘ └┘                 └────
st   ───────────────────────────────────────────────────┘└─
258      C_1, one_mul, finsupp.prod_single_index] at this,
id       └─┘  └─────┘  └───────────────────────┘
src  ───┘└─┘└┘└─────┘└┘└───────────────────────┘└───────┘
typ  ───┘└─┘└┘└─────┘└┘└───────────────────────┘└───────┘
doc  ───┘   └┘       └┘                         └───────┘
txt  ───┘   └┘       └┘                         └───────┘
par  ───┘   └┘       └┘                         └───────┘
pid  ───┘   └┘       └┘                         └──────┘
st   ──────┘└───────┘└─────────────────────────┘└──────┘└─
259    exact pow_zero _
id           └──────┘
src    └────┘└──────┘└─┘
typ    └────┘└──────┘└─┘
doc    └────┘        └─┘
txt    └────┘        └─┘
par    └────┘        └─┘
pid                 └┘
st   ──────────────────┘
260  end
st   └─┘
261  
262  lemma coeff_X' (i : σ) (m) :
id                       
typ                      
263    coeff m (X i : mv_polynomial σ α) = if single i 1 = m then 1 else 0 :=
id     └───┘       └───────────┘        └────┘     
src    └───┘         └───────────┘          └────┘     
typ    └───┘       └───────────┘        └────┘     
doc    └───┘         └───────────┘           └────┘
264  by rw [← coeff_X_pow, pow_one]
id            └─────────┘  └─────┘
src     └────┘└─────────┘└┘└─────┘└─
typ     └────┘└─────────┘└┘└─────┘└─
doc     └────┘           └┘       └─
txt     └────┘           └┘       └─
par     └────┘           └┘       └─
pid       └──┘           └┘       
st     └────────────────┘└───────┘
265  
src  
typ  
doc  
txt  
par  
pid  
st   
266  @[simp] lemma coeff_X (i : σ) :
id                              
typ                             
doc    └──┘
267    coeff (single i 1) (X i : mv_polynomial σ α) = 1 :=
id     └───┘  └────┘          └───────────┘    
src    └───┘  └────┘            └───────────┘      
typ    └───┘  └────┘          └───────────┘    
doc    └───┘  └────┘            └───────────┘
268  by rw [coeff_X', if_pos rfl]
id          └──────┘  └────┘ └─┘
src     └──┘└──────┘└┘└────┘└─┘└─
typ     └──┘└──────┘└┘└────┘└─┘└─
doc     └──┘        └┘         └─
txt     └──┘        └┘         └─
par     └──┘        └┘         └─
pid       └┘        └┘         
st     └───────────┘└──────────┘
269  
src  
typ  
doc  
txt  
par  
pid  
st   
270  @[simp] lemma coeff_C_mul (m) (a : α) (p : mv_polynomial σ α) : coeff m (C a * p) = a * coeff m p :=
id                                             └───────────┘      └───┘           └───┘  
src                                             └───────────┘        └───┘               └───┘
typ                                            └───────────┘      └───┘           └───┘  
doc    └──┘                                     └───────────┘        └───┘                  └───┘
271  begin
st   └─────
272    rw [mul_def, C, monomial],
id         └─────┘    └──────┘
src    └──┘└─────┘└┘└┘└──────┘
typ    └──┘└─────┘└┘└┘└──────┘
doc    └──┘       └┘└┘└──────┘
txt    └──┘       └┘ └┘        
par    └──┘       └┘ └┘        
pid      └┘       └┘ └┘        
st   ────────────┘└─┘└────────┘└──
273    simp only [sum_single_index, zero_mul, single_zero, zero_add, sum_zero],
id                └──────────────┘  └──────┘  └─────────┘  └──────┘  └──────┘
src    └─────────┘└──────────────┘└┘└──────┘└┘└─────────┘└┘└──────┘└┘└──────┘
typ    └─────────┘└──────────────┘└┘└──────┘└┘└─────────┘└┘└──────┘└┘└──────┘
doc    └─────────┘                └┘        └┘           └┘        └┘        
txt    └─────────┘                └┘        └┘           └┘        └┘        
par    └─────────┘                └┘        └┘           └┘        └┘        
pid        └──┘└┘                └┘        └┘           └┘        └┘        
st   ────────────────────────────────────────────────────────────────────────┘└─
274    convert sum_apply,
id             └───────┘
src    └──────┘└───────┘
typ    └──────┘└───────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ──────────────────┘└─
275    simp only [single_apply, finsupp.sum],
id                └──────────┘  └─────────┘
src    └─────────┘└──────────┘└┘└─────────┘
typ    └─────────┘└──────────┘└┘└─────────┘
doc    └─────────┘            └┘└─────────┘
txt    └─────────┘            └┘           
par    └─────────┘            └┘           
pid        └──┘└┘            └┘           
st   ──────────────────────────────────────┘└─
276    rw finset.sum_eq_single m,
id        └──────────────────┘ 
src    └─┘└──────────────────┘
typ    └─┘└──────────────────┘
doc    └─┘                    
txt    └─┘                    
par    └─┘                    
pid                          
st   ──────────────────────────┘└─
277    { rw if_pos rfl, refl },
id          └────┘ └─┘
src      └─┘└────┘└─┘  └───┘
typ      └─┘└────┘└─┘  └───┘
doc      └─┘           └───┘
txt      └─┘           └───┘
par      └─┘           └───┘
pid                       
st   ───┘└───────────┘└─────┘└┘
278    { intros m' hm' H, apply if_neg, exact H },
id                              └────┘        
src      └─────────────┘  └────┘└────┘  └────┘ 
typ      └─────────────┘  └────┘└────┘  └────┘
doc      └─────────────┘  └────┘        └────┘ 
txt      └─────────────┘  └────┘        └────┘ 
par      └─────────────┘  └────┘        └────┘ 
pid            └───────┘                     
st   ───┘└─────────────┘└────────────┘└────────┘└┘
279    { intros hm, rw if_pos rfl, rw not_mem_support_iff at hm, simp [hm] }
id                     └────┘ └─┘     └─────────────────┘              └┘
src      └───────┘  └─┘└────┘└─┘  └─┘└─────────────────┘└────┘  └────┘  └┘
typ      └───────┘  └─┘└────┘└─┘  └─┘└─────────────────┘└────┘  └────┘└┘└┘
doc      └───────┘  └─┘           └─┘                   └────┘  └────┘  └┘
txt      └───────┘  └─┘           └─┘                   └────┘  └────┘  └┘
par      └───────┘  └─┘           └─┘                   └────┘  └────┘  └┘
pid            └─┘                                    └────┘        
st   ────────────┘└─────────────┘└────────────────────────────┘└──────────┘└─
280  end
st   ──┘
281  
282  lemma coeff_mul (p q : mv_polynomial σ α) (n : σ →₀ ℕ) :
id                          └───────────┘          └┘ 
src                         └───────────┘             └┘ 
typ                         └───────────┘          └┘ 
doc                         └───────────┘             └┘
283    coeff n (p * q) = finset.sum (antidiagonal n).support (λ x, coeff x.1 p * coeff x.2 q) :=
id     └───┘        └────────┘  └──────────┘  └─────┘       └───┘     └───┘   
src    └───┘           └────────┘  └──────────┘   └─────┘        └───┘       └───┘  
typ    └───┘        └────────┘  └──────────┘  └─────┘       └───┘     └───┘   
doc    └───┘                                                       └───┘         └───┘
284  begin
st   └─────
285    rw mul_def,
id        └─────┘
src    └─┘└─────┘
typ    └─┘└─────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────┘└─
286    have := @finset.sum_sigma (σ →₀ ℕ) α _ _ p.support (λ _, q.support)
id              └──────────────┘   └┘         └───────┘       └───────┘
src    └──────┘ └──────────────┘  └┘ └┘ └───┘└───────┘  └──┘└───────┘└─
typ    └──────┘ └──────────────┘ └┘ └┘└───┘└───────┘  └──┘└───────┘└─
doc    └──────┘                   └┘ └┘ └───┘           └──┘         └─
txt    └──────┘                      └┘ └───┘           └──┘         └─
par    └──────┘                      └┘ └───┘           └──┘         └─
pid    └───┘└─┘                      └┘ └───┘           └──┘         └─
st   ──────────────────────────────────────────────────────────────────────
287      (λ x, if (x.1 + x.2 = n) then coeff x.1 p * coeff x.2 q else 0),
id                                              └───┘     
src  ───┘  └──┘    └─┘ └─┘ └─────┘      └─┘ └───┘ └─┘ └──────┘
typ  ───┘  └──┘    └─┘ └─┘└─────┘      └─┘└───┘ └─┘└──────┘
doc  ───┘  └──┘    └─┘  └─┘  └─────┘      └─┘  └───┘ └─┘ └──────┘
txt  ───┘  └──┘    └─┘  └─┘  └─────┘      └─┘        └─┘ └──────┘
par  ───┘  └──┘    └─┘  └─┘  └─────┘      └─┘        └─┘ └──────┘
pid  ───┘  └──┘    └─┘  └─┘  └─────┘      └─┘        └─┘ └──────┘
st   ──────────────────────────────────────────────────────────────────┘└─
288    convert this.symm using 1; clear this,
id             └───────┘
src    └──────┘└───────┘└──────┘  └────────┘
typ    └──────┘└───────┘└──────┘  └────────┘
doc    └──────┘         └──────┘  └────────┘
txt    └──────┘         └──────┘  └────────┘
par    └──────┘         └──────┘  └────────┘
pid                    └─────┘       └───┘
st   ──────────────────────────────────────┘└─
289    { rw [coeff],
id           └───┘
src      └──┘└───┘
typ      └──┘└───┘
doc      └──┘└───┘
txt      └──┘     
par      └──┘     
pid        └┘     
st   ───┘└───────┘└──
290      repeat {rw sum_apply, apply finset.sum_congr rfl, intros, dsimp only},
id                  └───────┘        └──────────────┘ └─┘
src      └──────┘└─┘└───────┘└┘└────┘└──────────────┘└─┘└┘└────┘└┘└────────┘
typ      └──────┘└─┘└───────┘└┘└────┘└──────────────┘└─┘└┘└────┘└┘└────────┘
doc      └──────┘└─┘         └┘└────┘                   └┘└────┘└┘└────────┘
txt      └──────┘└─┘         └┘└────┘                   └┘└────┘└┘└────────┘
par      └──────┘└─┘         └┘└────┘                   └┘└────┘└┘└────────┘
pid            └───┘         └──────┘                   └───────────────────┘
st   ───────────────────────┘└──────────────────────────┘└──────┘└──────────┘└┘
291      convert single_apply },
id               └──────────┘
src      └──────┘└──────────┘
typ      └──────┘└──────────┘
doc      └──────┘            
txt      └──────┘            
par      └──────┘            
pid                         
st   ────────────────────────┘└┘
292    { have : (antidiagonal n).support.filter (λ x, x.1 ∈ p.support ∧ x.2 ∈ q.support) ⊆
id                                                         └───────┘         └───────┘  
src      └─────┘              └───────────────┘  └──┘ └─┘└───────┘  └─┘ └───────┘└┘
typ      └─────┘              └───────────────┘  └──┘ └─┘└───────┘  └─┘ └───────┘└┘
doc      └─────┘              └───────────────┘  └──┘ └─┘            └─┘          └┘ 
txt      └─────┘              └───────────────┘  └──┘ └─┘            └─┘          └┘ 
par      └─────┘              └───────────────┘  └──┘ └─┘            └─┘          └┘ 
pid      └───┘└┘              └───────────────┘  └──┘ └─┘            └─┘          └┘ 
st   ──────────────────────────────────────────────────────────────────────────────────────
293             (antidiagonal n).support := finset.filter_subset _,
id               └──────────┘              └──────────────────┘
src  ──────────┘ └──────────┘ └───────────┘└──────────────────┘└┘
typ  ──────────┘ └──────────┘└───────────┘└──────────────────┘└┘
doc  ──────────┘              └───────────┘                    └┘
txt  ──────────┘              └───────────┘                    └┘
par  ──────────┘              └───────────┘                    └┘
pid  ──────────┘              └──────┘└───┘                    └┘
st   ────────────────────────────────────────────────────────────┘└─
294      rw [← finset.sum_sdiff this, finset.sum_eq_zero, zero_add], swap,
id             └──────────────┘ └──┘  └────────────────┘  └──────┘
src      └────┘└──────────────┘    └┘└────────────────┘└┘└──────┘  └──┘
typ      └────┘└──────────────┘└──┘└┘└────────────────┘└┘└──────┘  └──┘
doc      └────┘                    └┘                  └┘          └──┘
txt      └────┘                    └┘                  └┘          └──┘
par      └────┘                    └┘                  └┘          └──┘
pid        └──┘                    └┘                  └┘        
st   ──────────────────────────────┘└──────────────────┘└────────┘└─────┘└─
295      { intros x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid              └───┘
st   ─────┘└─────────┘└─
296        rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter),
id             └──────────────┘  └────────────────┘  └───────────────┘
src        └──┘└──────────────┘└┘└────────────────┘ └───────────────┘└──
typ        └──┘└──────────────┘└┘└────────────────┘ └───────────────┘└──
doc        └──┘                └┘                                    └──
txt        └──┘                └┘                                    └──
par        └──┘                └┘                                    └──
pid          └┘                └┘                                    └──
st   ─────────────────────────┘└──────────────────────────────────────┘└─
297            not_and, not_and, not_mem_support_iff] at hx,
id             └─────┘  └─────┘  └─────────────────┘
src  ─────────┘└─────┘└┘└─────┘└┘└─────────────────┘└─────┘
typ  ─────────┘└─────┘└┘└─────┘└┘└─────────────────┘└─────┘
doc  ─────────┘       └┘       └┘                   └─────┘
txt  ─────────┘       └┘       └┘                   └─────┘
par  ─────────┘       └┘       └┘                   └─────┘
pid  ─────────┘       └┘       └┘                   └────┘
st   ────────────────┘└───────┘└───────────────────┘└────┘└─
298        by_cases H : x.1 ∈ p.support,
id                           └───────┘
src        └───────┘ └─┘ └─┘ └───────┘
typ        └───────┘ └─┘└─┘ └───────┘
doc        └───────┘ └─┘ └─┘ 
txt        └───────┘ └─┘ └─┘ 
par        └───────┘ └─┘ └─┘ 
pid                 └─┘ └─┘ 
st   ─────────────────────────────────┘└─
299        { rw [coeff, coeff, hx.2 hx.1 H, mul_zero] },
id               └───┘  └───┘       └┘     └──────┘
src          └──┘└───┘└┘└───┘└┘  └─┘  └─┘ └┘└──────┘└┘
typ          └──┘└───┘└┘└───┘└┘  └─┘└┘└─┘└┘└──────┘└┘
doc          └──┘└───┘└┘└───┘└┘  └─┘  └─┘ └┘        └┘
txt          └──┘     └┘     └┘  └─┘  └─┘ └┘        └┘
par          └──┘     └┘     └┘  └─┘  └─┘ └┘        └┘
pid            └┘     └┘     └┘  └─┘  └─┘ └┘        
st   ───────┘└───────┘└─────┘└───────────┘└────────┘└┘
300        { rw not_mem_support_iff at H, rw [coeff, H, zero_mul] } },
id              └─────────────────┘           └───┘    └──────┘
src          └─┘└─────────────────┘└───┘  └──┘└───┘└┘ └┘└──────┘└┘
typ          └─┘└─────────────────┘└───┘  └──┘└───┘└┘└┘└──────┘└┘
doc          └─┘                   └───┘  └──┘└───┘└┘ └┘        └┘
txt          └─┘                   └───┘  └──┘     └┘ └┘        └┘
par          └─┘                   └───┘  └──┘     └┘ └┘        └┘
pid                               └───┘    └┘     └┘ └┘        
st   ──────────────────────────────────┘└─────────┘└─┘└────────┘└──┘
301      symmetry,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
st   ───────────┘└─
302      rw [← finset.sum_sdiff (finset.filter_subset _), finset.sum_eq_zero, zero_add], swap,
id             └──────────────┘  └──────────────────┘     └────────────────┘  └──────┘
src      └────┘└──────────────┘ └──────────────────┘└───┘└────────────────┘└┘└──────┘  └──┘
typ      └────┘└──────────────┘ └──────────────────┘└───┘└────────────────┘└┘└──────┘  └──┘
doc      └────┘                                     └───┘                  └┘          └──┘
txt      └────┘                                     └───┘                  └┘          └──┘
par      └────┘                                     └───┘                  └┘          └──┘
pid        └──┘                                     └───┘                  └┘        
st   ──────────────────────────────────────────────────┘└──────────────────┘└────────┘└─────┘└─
303      { intros x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid              └───┘
st   ─────┘└─────────┘└─
304        rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter), not_and] at hx,
id             └──────────────┘  └────────────────┘  └───────────────┘   └─────┘
src        └──┘└──────────────┘└┘└────────────────┘ └───────────────┘└─┘└─────┘└─────┘
typ        └──┘└──────────────┘└┘└────────────────┘ └───────────────┘└─┘└─────┘└─────┘
doc        └──┘                └┘                                    └─┘       └─────┘
txt        └──┘                └┘                                    └─┘       └─────┘
par        └──┘                └┘                                    └─┘       └─────┘
pid          └┘                └┘                                    └─┘       └────┘
st   ─────────────────────────┘└──────────────────────────────────────┘└───────┘└────┘└─
305        rw if_neg,
id            └────┘
src        └─┘└────┘
typ        └─┘└────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ──────────────┘└─
306        exact hx.2 hx.1 },
id                    └┘
src        └────┘  └─┘  └─┘
typ        └────┘  └─┘└┘└─┘
doc        └────┘  └─┘  └─┘
txt        └────┘  └─┘  └─┘
par        └────┘  └─┘  └─┘
pid               └─┘  └─┘
st   ─────────────────────┘└┘
307      { apply finset.sum_bij, swap 5,
id               └────────────┘
src        └────┘└────────────┘  └────┘
typ        └────┘└────────────┘  └────┘
doc        └────┘                └────┘
txt        └────┘                └────┘
par        └────┘                └────┘
pid                                 
st   ─────┘└──────────────────┘└──────┘└─
308        { intros x hx, exact (x.1, x.2) },
id                                    
src          └─────────┘  └────┘  └──┘ └──┘
typ          └─────────┘  └────┘  └──┘└──┘
doc          └─────────┘  └────┘  └──┘ └──┘
txt          └─────────┘  └────┘  └──┘ └──┘
par          └─────────┘  └────┘  └──┘ └──┘
pid                └───┘         └──┘ └─┘
st   ───────┘└─────────┘└─────────────────┘└┘
309        { intros x hx, rw [finset.mem_filter, finset.mem_sigma] at hx,
id                            └───────────────┘  └──────────────┘
src          └─────────┘  └──┘└───────────────┘└┘└──────────────┘└─────┘
typ          └─────────┘  └──┘└───────────────┘└┘└──────────────┘└─────┘
doc          └─────────┘  └──┘                 └┘                └─────┘
txt          └─────────┘  └──┘                 └┘                └─────┘
par          └─────────┘  └──┘                 └┘                └─────┘
pid                └───┘    └┘                 └┘                └────┘
st   ───────┘└─────────┘└─────────────────────┘└────────────────┘└────┘└─
310          simpa [finset.mem_filter, mem_antidiagonal_support] using hx.symm },
id                  └───────────────┘  └──────────────────────┘        └─────┘
src          └─────┘└───────────────┘└┘└──────────────────────┘└──────┘└─────┘
typ          └─────┘└───────────────┘└┘└──────────────────────┘└──────┘└─────┘
doc          └─────┘                 └┘                        └──────┘       
txt          └─────┘                 └┘                        └──────┘       
par          └─────┘                 └┘                        └──────┘       
pid                                └┘                        └────┘       
st   ─────────────────────────────────────────────────────────────────────────┘└┘
311        { intros x hx, rw finset.mem_filter at hx, rw if_pos hx.2 },
id                           └───────────────┘           └────┘ └┘
src          └─────────┘  └─┘└───────────────┘└────┘  └─┘└────┘  └─┘
typ          └─────────┘  └─┘└───────────────┘└────┘  └─┘└────┘└┘└─┘
doc          └─────────┘  └─┘                 └────┘  └─┘        └─┘
txt          └─────────┘  └─┘                 └────┘  └─┘        └─┘
par          └─────────┘  └─┘                 └────┘  └─┘        └─┘
pid                └───┘                     └────┘            └─┘
st   ───────┘└─────────┘└──────────────────────────┘└───────────────┘└┘
312        { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl, simpa using and.intro },
id                                                    └───────┘
src          └─────────────────────────┘  └──────────┘└───────┘
typ          └─────────────────────────┘  └──────────┘└───────┘
doc          └─────────────────────────┘  └──────────┘         
txt          └─────────────────────────┘  └──────────┘         
par          └─────────────────────────┘  └──────────┘         
pid                 └──────────────────┘       └────┘         
st   ───────┘└─────────────────────────┘└──────────────────────┘└┘
313        { rintros ⟨i,j⟩ hij, refine ⟨⟨i,j⟩, _, _⟩, { apply_instance },
id                                        
src          └───────────────┘  └─────┘    └──────┘    └─────────────┘
typ          └───────────────┘  └─────┘  └──────┘    └─────────────┘
doc          └───────────────┘  └─────┘    └──────┘    └─────────────┘
txt          └───────────────┘  └─────┘    └──────┘    └─────────────┘
par          └───────────────┘  └─────┘    └──────┘    └─────────────┘
pid                 └────────┘            └──────┘                  
st   ────────────────────────┘└────────────────────┘└──┘└─────────────┘└┘
314          { rw [finset.mem_filter, mem_antidiagonal_support] at hij,
id                 └───────────────┘  └──────────────────────┘
src            └──┘└───────────────┘└┘└──────────────────────┘└──────┘
typ            └──┘└───────────────┘└┘└──────────────────────┘└──────┘
doc            └──┘                 └┘                        └──────┘
txt            └──┘                 └┘                        └──────┘
par            └──┘                 └┘                        └──────┘
pid              └┘                 └┘                        └─────┘
st   ─────────┘└───────────────────┘└────────────────────────┘└─────┘└─
315            simpa [finset.mem_filter, finset.mem_sigma] using hij.symm },
id                    └───────────────┘  └──────────────┘        └──────┘
src            └─────┘└───────────────┘└┘└──────────────┘└──────┘└──────┘
typ            └─────┘└───────────────┘└┘└──────────────┘└──────┘└──────┘
doc            └─────┘                 └┘                └──────┘        
txt            └─────┘                 └┘                └──────┘        
par            └─────┘                 └┘                └──────┘        
pid                                  └┘                └────┘        
st   ────────────────────────────────────────────────────────────────────┘└┘
316          { refl } } },
src            └───┘
typ            └───┘
doc            └───┘
txt            └───┘
par            └───┘
pid                
st   ──────────────┘└────┘
317      all_goals { apply_instance } }
src      └──────────┘└─────────────┘└┘
typ      └──────────┘└─────────────┘└┘
doc      └──────────┘└─────────────┘└┘
txt      └──────────┘└─────────────┘└┘
par      └──────────┘└─────────────┘└┘
pid               └─────────────────┘
st   ──────────────────────────────┘└─
318  end
st   ──┘
319  
320  @[simp] lemma coeff_mul_X (m) (s : σ) (p : mv_polynomial σ α) :
id                                             └───────────┘  
src                                             └───────────┘
typ                                            └───────────┘  
doc    └──┘                                     └───────────┘
321    coeff (m + single s 1) (p * X s) = coeff m p :=
id     └───┘    └────┘            └───┘  
src    └───┘     └────┘               └───┘
typ    └───┘    └────┘            └───┘  
doc    └───┘      └────┘                 └───┘
322  begin
st   └─────
323    have : (m, single s 1) ∈ (m + single s 1).antidiagonal.support := mem_antidiagonal_support.2 rfl,
id                               └────┘                             └──────────────────────┘   └─┘
src    └─────┘ └┘       └──┘  └────┘ └──────────────────────────┘└──────────────────────┘└─┘└─┘
typ    └─────┘ └┘       └──┘ └────┘└──────────────────────────┘└──────────────────────┘└─┘└─┘
doc    └─────┘  └┘       └──┘    └────┘ └──────────────────────────┘                        └─┘
txt    └─────┘  └┘       └──┘           └──────────────────────────┘                        └─┘
par    └─────┘  └┘       └──┘           └──────────────────────────┘                        └─┘
pid    └───┘└┘  └┘       └──┘           └─────────────────────┘└───┘                        └─┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
324    rw [coeff_mul, ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
id         └───────┘    └─────────────────┘ └──┘  └───────────────┘  └──────────────────┘
src    └──┘└───────┘└──┘└─────────────────┘    └┘└───────────────┘ └──────────────────┘└──────
typ    └──┘└───────┘└──┘└─────────────────┘└──┘└┘└───────────────┘ └──────────────────┘└──────
doc    └──┘         └──┘                       └┘                                      └──────
txt    └──┘         └──┘                       └┘                                      └──────
par    └──┘         └──┘                       └┘                                      └──────
pid      └┘         └──┘                       └┘                                      └──────
st   ──────────────┘└──────────────────────────┘└────────────────────────────────────────────┘└─
325        finset.sum_eq_zero, add_zero, coeff_X, mul_one],
id         └────────────────┘  └──────┘  └─────┘  └─────┘
src  ─────┘└────────────────┘└┘└──────┘└┘└─────┘└┘└─────┘
typ  ─────┘└────────────────┘└┘└──────┘└┘└─────┘└┘└─────┘
doc  ─────┘                  └┘        └┘       └┘       
txt  ─────┘                  └┘        └┘       └┘       
par  ─────┘                  └┘        └┘       └┘       
pid  ─────┘                  └┘        └┘       └┘       
st   ───────────────────────┘└────────┘└───────┘└───────┘└──
326    rintros ⟨i,j⟩ hij,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid           └────────┘
st   ──────────────────┘└─
327    rw [finset.mem_erase, mem_antidiagonal_support] at hij,
id         └──────────────┘  └──────────────────────┘
src    └──┘└──────────────┘└┘└──────────────────────┘└──────┘
typ    └──┘└──────────────┘└┘└──────────────────────┘└──────┘
doc    └──┘                └┘                        └──────┘
txt    └──┘                └┘                        └──────┘
par    └──┘                └┘                        └──────┘
pid      └┘                └┘                        └─────┘
st   ─────────────────────┘└────────────────────────┘└─────┘└─
328    by_cases H : single s 1 = j,
id                  └────┘     
src    └───────┘ └─┘└────┘ └─┘
typ    └───────┘ └─┘└────┘└─┘
doc    └───────┘ └─┘└────┘ └─┘ 
txt    └───────┘ └─┘       └─┘ 
par    └───────┘ └─┘       └─┘ 
pid             └─┘       └─┘ 
st   ────────────────────────────┘└─
329    { subst j, simpa using hij },
id                           └─┘
src      └────┘   └──────────┘   
typ      └────┘  └──────────┘└─┘
doc      └────┘   └──────────┘   
txt      └────┘   └──────────┘   
par      └────┘   └──────────┘   
pid                   └────┘   
st   ───┘└─────┘└────────────────┘└┘
330    { rw [coeff_X', if_neg H, mul_zero] },
id           └──────┘  └────┘   └──────┘
src      └──┘└──────┘└┘└────┘ └┘└──────┘└┘
typ      └──┘└──────┘└┘└────┘└┘└──────┘└┘
doc      └──┘        └┘       └┘        └┘
txt      └──┘        └┘       └┘        └┘
par      └──┘        └┘       └┘        └┘
pid        └┘        └┘       └┘        
st   ───────────────┘└────────┘└────────┘└──
331  end
st   ──┘
332  
333  lemma coeff_mul_X' (m) (s : σ) (p : mv_polynomial σ α) :
id                                      └───────────┘  
src                                      └───────────┘
typ                                     └───────────┘  
doc                                      └───────────┘
334    coeff m (p * X s) = if s ∈ m.support then coeff (m - single s 1) p else 0 :=
id     └───┘              └──────┘      └───┘    └────┘     
src    └───┘                   └──────┘      └───┘     └────┘
typ    └───┘              └──────┘      └───┘    └────┘     
doc    └───┘                                    └───┘      └────┘
335  begin
st   └─────
336    split_ifs with h h,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid             └──────┘
st   ───────────────────┘└─
337    { conv_rhs {rw ← coeff_mul_X _ s},
id                      └─────────┘   
src      └────────┘└───┘└─────────┘└─┘ 
typ      └────────┘└───┘└─────────┘└─┘
txt      └────────┘└───┘           └─┘ 
par      └────────┘└───┘           └─┘ 
pid              └────┘           └─┘ 
st   ───┘└────────┘└──────────────────┘└┘
338      congr' 1, ext t,
src      └──────┘  └───┘
typ      └──────┘  └───┘
doc      └──────┘  └───┘
txt      └──────┘  └───┘
par      └──────┘  └───┘
pid                 └┘
st   ───────────┘└─────┘└─
339      by_cases hj : s = t,
id                       
src      └───────┘  └─┘ 
typ      └───────┘  └─┘
doc      └───────┘  └─┘  
txt      └───────┘  └─┘  
par      └───────┘  └─┘  
pid                └─┘  
st   ──────────────────────┘└─
340      { subst t, simp only [nat_sub_apply, add_apply, single_eq_same],
id                            └───────────┘  └───────┘  └────────────┘
src        └────┘   └─────────┘└───────────┘└┘└───────┘└┘└────────────┘
typ        └────┘  └─────────┘└───────────┘└┘└───────┘└┘└────────────┘
doc        └────┘   └─────────┘             └┘         └┘              
txt        └────┘   └─────────┘             └┘         └┘              
par        └────┘   └─────────┘             └┘         └┘              
pid                    └──┘└┘             └┘         └┘              
st   ─────┘└─────┘└────────────────────────────────────────────────────┘└─
341        refine (nat.sub_add_cancel $ nat.pos_of_ne_zero _).symm, rwa mem_support_iff at h },
id                 └────────────────┘   └────────────────┘              └─────────────┘
src        └─────┘ └────────────────┘ └────────────────┘└──────┘  └──┘└─────────────┘└────┘
typ        └─────┘ └────────────────┘ └────────────────┘└──────┘  └──┘└─────────────┘└────┘
doc        └─────┘                                      └──────┘  └──┘               └────┘
txt        └─────┘                                      └──────┘  └──┘               └────┘
par        └─────┘                                      └──────┘  └──┘               └────┘
pid                                                    └─────┘                    └───┘
st   ────────────────────────────────────────────────────────────┘└─────────────────────────┘└┘
342      { simp [single_eq_of_ne hj] } },
id               └─────────────┘ └┘
src        └────┘└─────────────┘  └┘
typ        └────┘└─────────────┘└┘└┘
doc        └────┘                 └┘
txt        └────┘                 └┘
par        └────┘                 └┘
pid                             
st   ───────────────────────────────┘└──┘
343    { delta coeff, rw ← not_mem_support_iff, intro hm, apply h,
id                         └─────────────────┘
src      └─────────┘  └───┘└─────────────────┘  └──────┘  └────┘
typ      └─────────┘  └───┘└─────────────────┘  └──────┘  └────┘
doc      └─────────┘  └───┘                     └──────┘  └────┘
txt      └─────────┘  └───┘                     └──────┘  └────┘
par      └─────────┘  └───┘                     └──────┘  └────┘
pid           └────┘    └─┘                          └─┘       
st   ──────────────┘└────────────────────────┘└────────┘└───────┘└─
344      have H := support_mul _ _ hm, simp only [finset.mem_bind] at H,
id                 └─────────┘     └┘             └─────────────┘
src      └────────┘└─────────┘└───┘    └─────────┘└─────────────┘└────┘
typ      └────────┘└─────────┘└───┘└┘  └─────────┘└─────────────┘└────┘
doc      └────────┘           └───┘    └─────────┘               └────┘
txt      └────────┘           └───┘    └─────────┘               └────┘
par      └────────┘           └───┘    └─────────┘               └────┘
pid      └────┘└─┘           └───┘        └──┘└┘               └──┘
st   ───────────────────────────────┘└────────────────────────────────┘└─
345      rcases H with ⟨j, hj, i', hi', H⟩,
id              
src      └─────┘ └───────────────────────┘
typ      └─────┘└───────────────────────┘
doc      └─────┘ └───────────────────────┘
txt      └─────┘ └───────────────────────┘
par      └─────┘ └───────────────────────┘
pid             └───────────────────────┘
st   ────────────────────────────────────┘└─
346      delta X monomial at hi', rw mem_support_single at hi', cases hi', subst i',
id                                   └────────────────┘               └─┘        └┘
src      └─────────────────────┘  └─┘└────────────────┘└─────┘  └────┘     └────┘
typ      └─────────────────────┘  └─┘└────────────────┘└─────┘  └────┘└─┘  └────┘└┘
doc      └─────────────────────┘  └─┘                  └─────┘  └────┘     └────┘
txt      └─────────────────────┘  └─┘                  └─────┘  └────┘     └────┘
par      └─────────────────────┘  └─┘                  └─────┘  └────┘     └────┘
pid           └─────────┘└─────┘                      └─────┘                 
st   ──────────────────────────┘└────────────────────────────┘└─────────┘└────────┘└─
347      erw finset.mem_singleton at H, subst m,
id           └──────────────────┘             
src      └──┘└──────────────────┘└───┘  └────┘
typ      └──┘└──────────────────┘└───┘  └────┘
doc      └──┘                    └───┘  └────┘
txt      └──┘                    └───┘  └────┘
par      └──┘                    └───┘  └────┘
pid                             └───┘       
st   ────────────────────────────────┘└───────┘└─
348      rw [mem_support_iff, add_apply, single_apply, if_pos rfl],
id           └─────────────┘  └───────┘  └──────────┘  └────┘ └─┘
src      └──┘└─────────────┘└┘└───────┘└┘└──────────┘└┘└────┘└─┘
typ      └──┘└─────────────┘└┘└───────┘└┘└──────────┘└┘└────┘└─┘
doc      └──┘               └┘         └┘            └┘         
txt      └──┘               └┘         └┘            └┘         
par      └──┘               └┘         └┘            └┘         
pid        └┘               └┘         └┘            └┘         
st   ──────────────────────┘└─────────┘└────────────┘└──────────┘└──
349      intro H, rw [_root_.add_eq_zero_iff] at H, exact one_ne_zero H.2 }
id                    └────────────────────┘              └─────────┘ 
src      └─────┘  └──┘└────────────────────┘└────┘  └────┘└─────────┘ └─┘
typ      └─────┘  └──┘└────────────────────┘└────┘  └────┘└─────────┘└─┘
doc      └─────┘  └──┘                      └────┘  └────┘            └─┘
txt      └─────┘  └──┘                      └────┘  └────┘            └─┘
par      └─────┘  └──┘                      └────┘  └────┘            └─┘
pid           └┘    └┘                      └───┘                   └─┘
st   ──────────┘└──────────────────────────┘└───┘└──────────────────────┘└─
350  end
st   ──┘
351  
352  end coeff
353  
354  section eval₂
355  variables [comm_semiring β]
id              └───────────┘
src             └───────────┘
typ             └───────────┘
356  variables (f : α → β) (g : σ → β)
id             
typ            
357  
358  /-- Evaluate a polynomial `p` given a valuation `g` of all the variables
359    and a ring hom `f` from the scalar ring to the target -/
360  def eval₂ (p : mv_polynomial σ α) : β :=
id                  └───────────┘      
src                 └───────────┘
typ                 └───────────┘      
doc                 └───────────┘
361  p.sum (λs a, f a * s.prod (λn e, g n ^ e))
id   └──┘         └───┘         
src   └──┘              └───┘            
typ  └──┘         └───┘         
doc   └──┘               └───┘
362  
363  @[simp] lemma eval₂_zero : (0 : mv_polynomial σ α).eval₂ f g = 0 :=
id                                   └───────────┘   └───┘    
src                                  └───────────┘     └───┘      
typ                                  └───────────┘   └───┘    
doc    └──┘                          └───────────┘     └───┘
364  finsupp.sum_zero_index
id   └────────────────────┘
src  └────────────────────┘
typ  └────────────────────┘
365  
366  section
367  variables [is_semiring_hom f]
id              └─────────────┘
src             └─────────────┘
typ             └─────────────┘
doc             └─────────────┘
368  
369  @[simp] lemma eval₂_add : (p + q).eval₂ f g = p.eval₂ f g + q.eval₂ f g :=
id                                 └───┘     └────┘    └────┘  
src                                  └───┘        └────┘       └────┘
typ                                └───┘     └────┘    └────┘  
doc    └──┘                           └───┘         └────┘        └────┘
370  finsupp.sum_add_index
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
371    (by simp [is_semiring_hom.map_zero f])
id               └──────────────────────┘ 
src        └────┘└──────────────────────┘ 
typ        └────┘└──────────────────────┘
doc        └────┘                         
txt        └────┘                         
par        └────┘                         
pid                                     
st        └────────────────────────────────┘
372    (by simp [add_mul, is_semiring_hom.map_add f])
id               └─────┘  └─────────────────────┘ 
src        └────┘└─────┘└┘└─────────────────────┘ 
typ        └────┘└─────┘└┘└─────────────────────┘
doc        └────┘       └┘                        
txt        └────┘       └┘                        
par        └────┘       └┘                        
pid                   └┘                        
st        └────────────────────────────────────────┘
373  
374  @[simp] lemma eval₂_monomial : (monomial s a).eval₂ f g = f a * s.prod (λn e, g n ^ e) :=
id                                   └──────┘   └───┘        └───┘         
src                                  └──────┘     └───┘             └───┘            
typ                                  └──────┘   └───┘        └───┘         
doc    └──┘                          └──────┘     └───┘               └───┘
375  finsupp.sum_single_index (by simp [is_semiring_hom.map_zero f])
id   └──────────────────────┘           └──────────────────────┘ 
src  └──────────────────────┘     └────┘└──────────────────────┘ 
typ  └──────────────────────┘     └────┘└──────────────────────┘
doc                               └────┘                         
txt                               └────┘                         
par                               └────┘                         
pid                                                            
st                               └────────────────────────────────┘
376  
377  @[simp] lemma eval₂_C (a) : (C a).eval₂ f g = f a :=
id                                  └───┘      
src                                  └───┘      
typ                                 └───┘      
doc    └──┘                          └───┘
378  by simp [eval₂_monomial, C, prod_zero_index]
id            └────────────┘    └─────────────┘
src     └────┘└────────────┘└┘└┘└─────────────┘└─
typ     └────┘└────────────┘└┘└┘└─────────────┘└─
doc     └────┘              └┘└┘               └─
txt     └────┘              └┘ └┘               └─
par     └────┘              └┘ └┘               └─
pid                       └┘ └┘               
st     └──────────────────────────────────────────
379  
src  
typ  
doc  
txt  
par  
pid  
st   
380  @[simp] lemma eval₂_one : (1 : mv_polynomial σ α).eval₂ f g = 1 :=
id                                  └───────────┘   └───┘    
src                                 └───────────┘     └───┘      
typ                                 └───────────┘   └───┘    
doc    └──┘                         └───────────┘     └───┘
381  (eval₂_C _ _ _).trans (is_semiring_hom.map_one f)
id    └─────┘       └───┘   └─────────────────────┘ 
src   └─────┘       └───┘   └─────────────────────┘
typ   └─────┘       └───┘   └─────────────────────┘ 
382  
383  @[simp] lemma eval₂_X (n) : (X n).eval₂ f g = g n :=
id                                  └───┘      
src                                  └───┘      
typ                                 └───┘      
doc    └──┘                          └───┘
384  by simp [eval₂_monomial,
id            └────────────┘
src     └────┘└────────────┘└─
typ     └────┘└────────────┘└─
doc     └────┘              └─
txt     └────┘              └─
par     └────┘              └─
pid                       └─
st     └──────────────────────
385    is_semiring_hom.map_one f, X, prod_single_index, pow_one]
id     └─────────────────────┘     └───────────────┘  └─────┘
src  ─┘└─────────────────────┘ └┘└┘└───────────────┘└┘└─────┘└─
typ  ─┘└─────────────────────┘└┘└┘└───────────────┘└┘└─────┘└─
doc  ─┘                        └┘└┘                 └┘       └─
txt  ─┘                        └┘ └┘                 └┘       └─
par  ─┘                        └┘ └┘                 └┘       └─
pid  ─┘                        └┘ └┘                 └┘       
st   ────────────────────────────────────────────────────────────
386  
src  
typ  
doc  
txt  
par  
pid  
st   
387  lemma eval₂_mul_monomial :
388    ∀{s a}, (p * monomial s a).eval₂ f g = p.eval₂ f g * f a * s.prod (λn e, g n ^ e) :=
id              └──────┘   └───┘     └────┘       └───┘         
src                └──────┘     └───┘        └────┘            └───┘            
typ             └──────┘   └───┘     └────┘       └───┘         
doc                 └──────┘     └───┘         └────┘              └───┘
389  begin
st   └─────
390    apply mv_polynomial.induction_on p,
id           └────────────────────────┘ 
src    └────┘└────────────────────────┘
typ    └────┘└────────────────────────┘
doc    └────┘                          
txt    └────┘                          
par    └────┘                          
pid                                   
st   ───────────────────────────────────┘└─
391    { assume a' s a,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid      └───────────┘
st   ───┘└───────────┘└─
392      simp [C_mul_monomial, eval₂_monomial, is_semiring_hom.map_mul f] },
id             └────────────┘  └────────────┘  └─────────────────────┘ 
src      └────┘└────────────┘└┘└────────────┘└┘└─────────────────────┘ └┘
typ      └────┘└────────────┘└┘└────────────┘└┘└─────────────────────┘└┘
doc      └────┘              └┘              └┘                        └┘
txt      └────┘              └┘              └┘                        └┘
par      └────┘              └┘              └┘                        └┘
pid                        └┘              └┘                        
st   ────────────────────────────────────────────────────────────────────┘└┘
393    { assume p q ih_p ih_q, simp [add_mul, eval₂_add, ih_p, ih_q] },
id                                   └─────┘  └───────┘
src      └──────────────────┘  └────┘└─────┘└┘└───────┘└┘    └┘    └┘
typ      └──────────────────┘  └────┘└─────┘└┘└───────┘└┘└──┘└┘└──┘└┘
doc      └──────────────────┘  └────┘       └┘         └┘    └┘    └┘
txt      └──────────────────┘  └────┘       └┘         └┘    └┘    └┘
par      └──────────────────┘  └────┘       └┘         └┘    └┘    └┘
pid      └──────────────────┘             └┘         └┘    └┘    
st   ───┘└──────────────────┘└──────────────────────────────────────┘└┘
394    { assume p n ih s a,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid      └───────────────┘
st   ────────────────────┘└─
395      from calc (p * X n * monomial s a).eval₂ f g = (p * monomial (single n 1 + s) a).eval₂ f g :
id                                                                              
src      └───┘                  └──────┘                      └─┘ └┘ └──────┘  └──
typ      └───┘                  └──────┘                      └─┘ └┘ └──────┘  └──
doc      └───┘                   └──────┘                      └─┘  └┘ └──────┘  └──
txt      └───┘                    └──────┘                      └─┘  └┘ └──────┘  └──
par      └───┘                    └──────┘                      └─┘  └┘ └──────┘  └──
pid      └───┘                    └──────┘                      └─┘  └┘ └──────┘  └──
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
396          by simp [monomial_single_add, -add_comm, pow_one, mul_assoc]
id                    └─────────────────┘             └─────┘  └───────┘
src  ───────┘  └────┘└─────────────────┘└───────────┘└─────┘└┘└───────┘└─
typ  ───────┘  └────┘└─────────────────┘└───────────┘└─────┘└┘└───────┘└─
doc  ───────┘  └────┘                   └───────────┘       └┘         └─
txt  ───────┘  └────┘                   └───────────┘       └┘         └─
par  ───────┘  └────┘                   └───────────┘       └┘         └─
pid  ───────┘  └─────┘                   └───────────┘       └┘         └─
st   ─────────┘└──────────────────────────────────────────────────────────
397        ... = (p * monomial (single n 1) 1).eval₂ f g * f a * s.prod (λn e, g n ^ e) :
id                   └──────┘  └────┘                        └────┘           
src  ─────┘└──┘    └──────┘ └────┘ └───────────┘      └────┘  └───┘   └───
typ  ─────┘└──┘   └──────┘ └────┘└───────────┘    └────┘  └───┘  └───
doc  ─────┘└──┘    └──────┘ └────┘ └───────────┘      └────┘  └───┘    └───
txt  ─────┘└──┘                    └───────────┘              └───┘    └───
par  ─────┘└──┘                    └───────────┘              └───┘    └───
pid  ─────────┘                    └───────────┘              └───┘    └───
st   ─────┘└──────────────────────────────────────────────────────────────────────────────
398          by simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
id                        └───────────────┘  └────────────┘  └─────┘  └─────┘  └───────┘  └───────────┘
src  ───────┘  └────┘  └┘└───────────────┘└┘└────────────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└───────────┘└─
typ  ───────┘  └────┘└┘└┘└───────────────┘└┘└────────────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└───────────┘└─
doc  ───────┘  └────┘  └┘                 └┘              └┘       └┘       └┘         └┘             └─
txt  ───────┘  └────┘  └┘                 └┘              └┘       └┘       └┘         └┘             └─
par  ───────┘  └────┘  └┘                 └┘              └┘       └┘       └┘         └┘             └─
pid  ───────┘  └─────┘  └┘                 └┘              └┘       └┘       └┘         └┘             └─
st   ─────────┘└─────────────────────────────────────────────────────────────────────────────────────────
399            is_semiring_hom.map_one f, -add_comm] }
id             └─────────────────────┘ 
src  ─────────┘└─────────────────────┘ └───────────┘
typ  ─────────┘└─────────────────────┘└───────────┘
doc  ─────────┘                        └───────────┘
txt  ─────────┘                        └───────────┘
par  ─────────┘                        └───────────┘
pid  ─────────┘                        └───────────┘
st   ───────────────────────────────────────────────┘└─
400  end
st   ──┘
401  
402  @[simp] lemma eval₂_mul : ∀{p}, (p * q).eval₂ f g = p.eval₂ f g * q.eval₂ f g :=
id                                      └───┘     └────┘    └────┘  
src                                        └───┘        └────┘       └────┘
typ                                     └───┘     └────┘    └────┘  
doc    └──┘                                 └───┘         └────┘        └────┘
403  begin
st   └─────
404    apply mv_polynomial.induction_on q,
id           └────────────────────────┘ 
src    └────┘└────────────────────────┘
typ    └────┘└────────────────────────┘
doc    └────┘                          
txt    └────┘                          
par    └────┘                          
pid                                   
st   ───────────────────────────────────┘└─
405    { simp [C, eval₂_monomial, eval₂_mul_monomial, prod_zero_index] },
id               └────────────┘  └────────────────┘  └─────────────┘
src      └────┘└┘└────────────┘└┘└────────────────┘└┘└─────────────┘└┘
typ      └────┘└┘└────────────┘└┘└────────────────┘└┘└─────────────┘└┘
doc      └────┘└┘              └┘                  └┘               └┘
txt      └────┘ └┘              └┘                  └┘               └┘
par      └────┘ └┘              └┘                  └┘               └┘
pid           └┘              └┘                  └┘               
st   ───┘└────────────────────────────────────────────────────────────┘└┘
406    { simp [mul_add, eval₂_add] {contextual := tt} },
id             └─────┘  └───────┘                 └┘
src      └────┘└─────┘└┘└───────┘└┘ └────────────┘└┘└┘
typ      └────┘└─────┘└┘└───────┘└┘ └────────────┘└┘└┘
doc      └────┘       └┘         └┘ └────────────┘  └┘
txt      └────┘       └┘         └┘ └────────────┘  └┘
par      └────┘       └┘         └┘ └────────────┘  └┘
pid                 └┘          └────────────┘  
st   ───┘└───────────────────────────────────────────┘└┘
407    { simp [X, eval₂_monomial, eval₂_mul_monomial, (mul_assoc _ _ _).symm] { contextual := tt} }
id               └────────────┘  └────────────────┘   └───────┘                              └┘
src      └────┘└┘└────────────┘└┘└────────────────┘└┘ └───────┘└────────────┘ └─────────────┘└┘└┘
typ      └────┘└┘└────────────┘└┘└────────────────┘└┘ └───────┘└────────────┘ └─────────────┘└┘└┘
doc      └────┘└┘              └┘                  └┘          └────────────┘ └─────────────┘  └┘
txt      └────┘ └┘              └┘                  └┘          └────────────┘ └─────────────┘  └┘
par      └────┘ └┘              └┘                  └┘          └────────────┘ └─────────────┘  └┘
pid           └┘              └┘                  └┘          └───────────┘ └─────────────┘  
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
408  end
st   ──┘
409  
410  @[simp] lemma eval₂_pow {p:mv_polynomial σ α} : ∀{n:ℕ}, (p ^ n).eval₂ f g = (p.eval₂ f g)^n
id                              └───────────┘                └───┘      └────┘   
src                             └───────────┘                     └───┘         └────┘     
typ                             └───────────┘                └───┘      └────┘   
doc    └──┘                     └───────────┘                       └───┘          └────┘
411  | 0       := eval₂_one _ _
id                └───────┘
src               └───────┘
typ               └───────┘
412  | (n + 1) := by rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
id                      └─────┘  └─────┘  └─────┘  └─────┘  └───────┘
src                 └──┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘         └─
typ                 └──┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└───────┘└─
doc                  └──┘       └┘       └┘       └┘       └┘         └┘         └─
txt                  └──┘       └┘       └┘       └┘       └┘         └┘         └─
par                  └──┘       └┘       └┘       └┘       └┘         └┘         └─
pid                    └┘       └┘       └┘       └┘       └┘         └┘         
st                  └──────────┘└───────┘└───────┘└───────┘└─────────┘└─────────┘
413  
src  
typ  
doc  
txt  
par  
pid  
st   
414  instance eval₂.is_semiring_hom : is_semiring_hom (eval₂ f g) :=
id                                    └─────────────┘  └───┘  
src                                   └─────────────┘  └───┘
typ                                   └─────────────┘  └───┘  
doc                                   └─────────────┘  └───┘
415  { map_zero := eval₂_zero _ _,
id                 └────────┘
src                └────────┘
typ                └────────┘
416    map_one := eval₂_one _ _,
id                └───────┘
src               └───────┘
typ               └───────┘
417    map_add := λ p q, eval₂_add _ _,
id                     └───────┘
src                      └───────┘
typ                    └───────┘
418    map_mul := λ p q, eval₂_mul _ _ }
id                     └───────┘
src                      └───────┘
typ                    └───────┘
419  end
420  
421  lemma eval₂_comp_left {γ} [comm_semiring γ]
id                              └───────────┘ 
src                             └───────────┘
typ                             └───────────┘ 
422    (k : β → γ) [is_semiring_hom k]
id                └─────────────┘ 
src                 └─────────────┘
typ               └─────────────┘ 
doc                 └─────────────┘
423    (f : α → β) [is_semiring_hom f] (g : σ → β)
id                └─────────────┘           
src                 └─────────────┘
typ               └─────────────┘           
doc                 └─────────────┘
424    (p) : k (eval₂ f g p) = eval₂ (k ∘ f) (k ∘ g) p :=
id             └───┘      └───┘           
src             └───┘         └───┘           
typ            └───┘      └───┘           
doc             └───┘          └───┘
425  by apply mv_polynomial.induction_on p; simp [
id            └────────────────────────┘ 
src     └────┘└────────────────────────┘   └──────
typ     └────┘└────────────────────────┘  └──────
doc     └────┘                             └──────
txt     └────┘                             └──────
par     └────┘                             └──────
pid                                           └─
st     └───────────────────────────────────────────
426    eval₂_add, is_semiring_hom.map_add k,
id     └───────┘  └─────────────────────┘ 
src  ─┘└───────┘└┘└─────────────────────┘ └─
typ  ─┘└───────┘└┘└─────────────────────┘└─
doc  ─┘         └┘                        └─
txt  ─┘         └┘                        └─
par  ─┘         └┘                        └─
pid  ─┘         └┘                        └─
st   ────────────────────────────────────────
427    eval₂_mul, is_semiring_hom.map_mul k] {contextual := tt}
id     └───────┘  └─────────────────────┘                  └┘
src  ─┘└───────┘└┘└─────────────────────┘ └┘ └────────────┘└┘└─
typ  ─┘└───────┘└┘└─────────────────────┘└┘ └────────────┘└┘└─
doc  ─┘         └┘                        └┘ └────────────┘  └─
txt  ─┘         └┘                        └┘ └────────────┘  └─
par  ─┘         └┘                        └┘ └────────────┘  └─
pid  ─┘         └┘                         └────────────┘  
st   ───────────────────────────────────────────────────────────
428  
src  
typ  
doc  
txt  
par  
pid  
st   
429  @[simp] lemma eval₂_eta (p : mv_polynomial σ α) : eval₂ C X p = p :=
id                                └───────────┘      └───┘     
src                               └───────────┘        └───┘     
typ                               └───────────┘      └───┘     
doc    └──┘                       └───────────┘        └───┘  
430  by apply mv_polynomial.induction_on p;
id            └────────────────────────┘ 
src     └────┘└────────────────────────┘
typ     └────┘└────────────────────────┘
doc     └────┘                          
txt     └────┘                          
par     └────┘                          
pid                                    
st     └────────────────────────────────────
431     simp [eval₂_add, eval₂_mul] {contextual := tt}
id            └───────┘  └───────┘                 └┘
src     └────┘└───────┘└┘└───────┘└┘ └────────────┘└┘└─
typ     └────┘└───────┘└┘└───────┘└┘ └────────────┘└┘└─
doc     └────┘         └┘         └┘ └────────────┘  └─
txt     └────┘         └┘         └┘ └────────────┘  └─
par     └────┘         └┘         └┘ └────────────┘  └─
pid                  └┘          └────────────┘  
st   ──────────────────────────────────────────────────
432  
src  
typ  
doc  
txt  
par  
pid  
st   
433  lemma eval₂_congr (g₁ g₂ : σ → β)
id                                 
typ                                
434    (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i) :
id                         └┘      └──────┘   └───┘        └┘   └┘ 
src                          └┘        └──────┘   └───┘               
typ                        └┘      └──────┘   └───┘        └┘   └┘ 
doc                          └┘                     └───┘
435    p.eval₂ f g₁ = p.eval₂ f g₂ :=
id     └────┘  └┘  └────┘  └┘
src     └────┘        └────┘
typ    └────┘  └┘  └────┘  └┘
doc     └────┘         └────┘
436  begin
st   └─────
437    apply finset.sum_congr rfl,
id           └──────────────┘ └─┘
src    └────┘└──────────────┘└─┘
typ    └────┘└──────────────┘└─┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   ───────────────────────────┘└─
438    intros c hc, dsimp, congr' 1,
src    └─────────┘  └───┘  └──────┘
typ    └─────────┘  └───┘  └──────┘
doc    └─────────┘  └───┘  └──────┘
txt    └─────────┘  └───┘  └──────┘
par    └─────────┘  └───┘  └──────┘
pid          └───┘               
st   ────────────┘└─────┘└────────┘└─
439    apply finset.prod_congr rfl,
id           └───────────────┘ └─┘
src    └────┘└───────────────┘└─┘
typ    └────┘└───────────────┘└─┘
doc    └────┘                 
txt    └────┘                 
par    └────┘                 
pid                          
st   ────────────────────────────┘└─
440    intros i hi, dsimp, congr' 1,
src    └─────────┘  └───┘  └──────┘
typ    └─────────┘  └───┘  └──────┘
doc    └─────────┘  └───┘  └──────┘
txt    └─────────┘  └───┘  └──────┘
par    └─────────┘  └───┘  └──────┘
pid          └───┘               
st   ────────────┘└─────┘└────────┘└─
441    apply h hi,
id            └┘
src    └────┘ 
typ    └────┘└┘
doc    └────┘ 
txt    └────┘ 
par    └────┘ 
pid          
st   ───────────┘└─
442    rwa finsupp.mem_support_iff at hc
id         └─────────────────────┘
src    └──┘└─────────────────────┘└─────┘
typ    └──┘└─────────────────────┘└─────┘
doc    └──┘                       └─────┘
txt    └──┘                       └─────┘
par    └──┘                       └─────┘
pid                              └────┘
st   ───────────────────────────────────┘
443  end
st   └─┘
444  
445  variables [is_semiring_hom f]
id              └─────────────┘
src             └─────────────┘
typ             └─────────────┘
doc             └─────────────┘
446  
447  @[simp] lemma eval₂_prod (s : finset γ) (p : γ → mv_polynomial σ α) :
id                                 └────┘           └───────────┘  
src                                └────┘             └───────────┘
typ                                └────┘           └───────────┘  
doc    └──┘                        └────┘             └───────────┘
448    eval₂ f g (s.prod p) = s.prod (λ x, eval₂ f g $ p x) :=
id     └───┘    └───┘    └───┘      └───┘      
src    └───┘       └───┘      └───┘       └───┘
typ    └───┘    └───┘    └───┘      └───┘      
doc    └───┘       └───┘       └───┘       └───┘
449  (s.prod_hom _).symm
id    └───────┘   └──┘
src    └───────┘   └──┘
typ   └───────┘   └──┘
450  
451  @[simp] lemma eval₂_sum (s : finset γ) (p : γ → mv_polynomial σ α) :
id                                └────┘           └───────────┘  
src                               └────┘             └───────────┘
typ                               └────┘           └───────────┘  
doc    └──┘                       └────┘             └───────────┘
452    eval₂ f g (s.sum p) = s.sum (λ x, eval₂ f g $ p x) :=
id     └───┘    └──┘    └──┘      └───┘      
src    └───┘       └──┘      └──┘       └───┘
typ    └───┘    └──┘    └──┘      └───┘      
doc    └───┘                             └───┘
453  (s.sum_hom _).symm
id    └──────┘   └──┘
src    └──────┘   └──┘
typ   └──────┘   └──┘
454  
455  attribute [to_additive] eval₂_prod
id                           └────────┘
src                          └────────┘
typ                          └────────┘
doc             └─────────┘
456  
457  lemma eval₂_assoc (q : γ → mv_polynomial σ α) (p : mv_polynomial γ α) :
id                             └───────────┘         └───────────┘  
src                             └───────────┘           └───────────┘
typ                            └───────────┘         └───────────┘  
doc                             └───────────┘           └───────────┘
458    eval₂ f (λ t, eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p) :=
id     └───┘       └───┘          └───┘    └───┘   
src    └───┘         └───┘               └───┘      └───┘ 
typ    └───┘       └───┘          └───┘    └───┘   
doc    └───┘         └───┘                └───┘      └───┘ 
459  by { rw eval₂_comp_left (eval₂ f g), congr, funext, simp }
id           └─────────────┘  └───┘  
src       └─┘└─────────────┘ └───┘    └───┘  └────┘  └───┘
typ       └─┘└─────────────┘ └───┘  └───┘  └────┘  └───┘
doc       └─┘                └───┘           └────┘  └───┘
txt       └─┘                         └───┘  └────┘  └───┘
par       └─┘                         └───┘  └────┘  └───┘
pid                                                     
st     └───────────────────────────────┘└─────┘└──────┘└─────┘└┘
460  
461  end eval₂
462  
463  section eval
464  variables {f : σ → α}
465  
466  /-- Evaluate a polynomial `p` given a valuation `f` of all the variables -/
467  def eval (f : σ → α) : mv_polynomial σ α → α := eval₂ id f
id                        └───────────┘         └───┘ └┘ 
src                         └───────────┘            └───┘ └┘
typ                       └───────────┘         └───┘ └┘ 
doc                         └───────────┘            └───┘
468  
469  @[simp] lemma eval_zero : (0 : mv_polynomial σ α).eval f = 0 := eval₂_zero _ _
id                                  └───────────┘   └──┘         └────────┘
src                                 └───────────┘     └──┘          └────────┘
typ                                 └───────────┘   └──┘         └────────┘
doc    └──┘                         └───────────┘     └──┘
470  
471  @[simp] lemma eval_add : (p + q).eval f = p.eval f + q.eval f := eval₂_add _ _
id                                └──┘    └───┘   └───┘     └───────┘
src                                 └──┘      └───┘     └───┘      └───────┘
typ                               └──┘    └───┘   └───┘     └───────┘
doc    └──┘                          └──┘       └───┘      └───┘
472  
473  lemma eval_monomial : (monomial s a).eval f = a * s.prod (λn e, f n ^ e) :=
id                          └──────┘   └──┘      └───┘         
src                         └──────┘     └──┘         └───┘            
typ                         └──────┘   └──┘      └───┘         
doc                         └──────┘     └──┘           └───┘
474  eval₂_monomial _ _
id   └────────────┘
src  └────────────┘
typ  └────────────┘
475  
476  @[simp] lemma eval_C : ∀ a, (C a).eval f = a := eval₂_C _ _
id                                 └──┘        └─────┘
src                                  └──┘          └─────┘
typ                                └──┘        └─────┘
doc    └──┘                          └──┘
477  
478  @[simp] lemma eval_X : ∀ n, (X n).eval f = f n := eval₂_X _ _
id                                 └──┘         └─────┘
src                                  └──┘            └─────┘
typ                                └──┘         └─────┘
doc    └──┘                          └──┘
479  
480  @[simp] lemma eval_mul : (p * q).eval f = p.eval f * q.eval f := eval₂_mul _ _
id                                └──┘    └───┘   └───┘     └───────┘
src                                 └──┘      └───┘     └───┘      └───────┘
typ                               └──┘    └───┘   └───┘     └───────┘
doc    └──┘                          └──┘       └───┘      └───┘
481  
482  instance eval.is_semiring_hom : is_semiring_hom (eval f) :=
id                                   └─────────────┘  └──┘ 
src                                  └─────────────┘  └──┘
typ                                  └─────────────┘  └──┘ 
doc                                  └─────────────┘  └──┘
483  eval₂.is_semiring_hom _ _
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
484  
485  theorem eval_assoc {τ}
486    (f : σ → mv_polynomial τ α) (g : τ → α)
id             └───────────┘            
src             └───────────┘
typ            └───────────┘            
doc             └───────────┘
487    (p : mv_polynomial σ α) :
id          └───────────┘  
src         └───────────┘
typ         └───────────┘  
doc         └───────────┘
488    p.eval (eval g ∘ f) = (eval₂ C f p).eval g :=
id     └───┘  └──┘       └───┘    └──┘  
src     └───┘  └──┘         └───┘      └──┘
typ    └───┘  └──┘       └───┘    └──┘  
doc     └───┘  └──┘           └───┘      └──┘
489  begin
st   └─────
490    rw eval₂_comp_left (eval g),
id        └─────────────┘  └──┘ 
src    └─┘└─────────────┘ └──┘ 
typ    └─┘└─────────────┘ └──┘
doc    └─┘                └──┘ 
txt    └─┘                     
par    └─┘                     
pid                           
st   ────────────────────────────┘└─
491    unfold eval, congr; funext a; simp
src    └─────────┘  └───┘  └──────┘  └───┘
typ    └─────────┘  └───┘  └──────┘  └───┘
doc    └─────────┘         └──────┘  └───┘
txt    └─────────┘  └───┘  └──────┘  └───┘
par    └─────────┘  └───┘  └──────┘  └───┘
pid          └───┘               └┘      
st   ────────────┘└──────────────────────┘
492  end
st   └─┘
493  
494  end eval
495  
496  section map
497  variables [comm_semiring β]
id              └───────────┘
src             └───────────┘
typ             └───────────┘
498  variables (f : α → β)
499  
500  /-- `map f p` maps a polynomial `p` across a ring hom `f` -/
501  def map : mv_polynomial σ α → mv_polynomial σ β := eval₂ (C ∘ f) X
id             └───────────┘     └───────────┘      └───┘      
src            └───────────┘       └───────────┘        └───┘       
typ            └───────────┘     └───────────┘      └───┘      
doc            └───────────┘       └───────────┘        └───┘        
502  
503  variables [is_semiring_hom f]
id              └─────────────┘
src             └─────────────┘
typ             └─────────────┘
doc             └─────────────┘
504  
505  @[simp] theorem map_monomial (s : σ →₀ ℕ) (a : α) : map f (monomial s a) = monomial s (f a) :=
id                                      └┘            └─┘   └──────┘     └──────┘    
src                                      └┘             └─┘    └──────┘       └──────┘
typ                                     └┘            └─┘   └──────┘     └──────┘    
doc    └──┘                              └┘              └─┘    └──────┘        └──────┘
506  (eval₂_monomial _ _).trans monomial_eq.symm
id    └────────────┘     └───┘  └─────────┘└───┘
src   └────────────┘     └───┘  └─────────┘└───┘
typ   └────────────┘     └───┘  └─────────┘└───┘
507  
508  @[simp] theorem map_C : ∀ (a : α), map f (C a : mv_polynomial σ α) = C (f a) := map_monomial _ _
id                                     └─┘       └───────────┘             └──────────┘
src                                     └─┘         └───────────┘                 └──────────┘
typ                                    └─┘       └───────────┘             └──────────┘
doc    └──┘                             └─┘         └───────────┘        
509  
510  @[simp] theorem map_X : ∀ (n : σ), map f (X n : mv_polynomial σ α) = X n := eval₂_X _ _
id                                     └─┘       └───────────┘          └─────┘
src                                     └─┘         └───────────┘             └─────┘
typ                                    └─┘       └───────────┘          └─────┘
doc    └──┘                             └─┘         └───────────┘        
511  
512  @[simp] theorem map_one : map f (1 : mv_polynomial σ α) = 1 := eval₂_one _ _
id                             └─┘       └───────────┘          └───────┘
src                            └─┘        └───────────┘            └───────┘
typ                            └─┘       └───────────┘          └───────┘
doc    └──┘                    └─┘        └───────────┘
513  
514  @[simp] theorem map_add (p q : mv_polynomial σ α) :
id                                  └───────────┘  
src                                 └───────────┘
typ                                 └───────────┘  
doc    └──┘                         └───────────┘
515    map f (p + q) = map f p + map f q := eval₂_add _ _
id     └─┘        └─┘    └─┘      └───────┘
src    └─┘           └─┘      └─┘        └───────┘
typ    └─┘        └─┘    └─┘      └───────┘
doc    └─┘             └─┘       └─┘
516  
517  @[simp] theorem map_mul (p q : mv_polynomial σ α) :
id                                  └───────────┘  
src                                 └───────────┘
typ                                 └───────────┘  
doc    └──┘                         └───────────┘
518    map f (p * q) = map f p * map f q := eval₂_mul _ _
id     └─┘        └─┘    └─┘      └───────┘
src    └─┘           └─┘      └─┘        └───────┘
typ    └─┘        └─┘    └─┘      └───────┘
doc    └─┘             └─┘       └─┘
519  
520  @[simp] lemma map_pow (p : mv_polynomial σ α) (n : ℕ) :
id                              └───────────┘         
src                             └───────────┘           
typ                             └───────────┘         
doc    └──┘                     └───────────┘
521    map f (p^n) = (map f p)^n := eval₂_pow _ _
id     └─┘       └─┘       └───────┘
src    └─┘          └─┘          └───────┘
typ    └─┘       └─┘       └───────┘
doc    └─┘            └─┘
522  
523  instance map.is_semiring_hom :
524    is_semiring_hom (map f : mv_polynomial σ α → mv_polynomial σ β) :=
id     └─────────────┘  └─┘    └───────────┘     └───────────┘  
src    └─────────────┘  └─┘     └───────────┘       └───────────┘
typ    └─────────────┘  └─┘    └───────────┘     └───────────┘  
doc    └─────────────┘  └─┘     └───────────┘       └───────────┘
525  eval₂.is_semiring_hom _ _
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
526  
527  theorem map_id : ∀ (p : mv_polynomial σ α), map id p = p := eval₂_eta
id                           └───────────┘     └─┘ └┘       └───────┘
src                          └───────────┘       └─┘ └┘         └───────┘
typ                          └───────────┘     └─┘ └┘       └───────┘
doc                          └───────────┘       └─┘
528  
529  theorem map_map [comm_semiring γ]
id                    └───────────┘ 
src                   └───────────┘
typ                   └───────────┘ 
530    (g : β → γ) [is_semiring_hom g]
id                └─────────────┘ 
src                 └─────────────┘
typ               └─────────────┘ 
doc                 └─────────────┘
531    (p : mv_polynomial σ α) :
id          └───────────┘  
src         └───────────┘
typ         └───────────┘  
doc         └───────────┘
532    map g (map f p) = map (g ∘ f) p :=
id     └─┘   └─┘     └─┘      
src    └─┘    └─┘       └─┘    
typ    └─┘   └─┘     └─┘      
doc    └─┘    └─┘        └─┘
533  (eval₂_comp_left (map g) (C ∘ f) X p).trans $
id    └─────────────┘  └─┘          └───┘
src   └─────────────┘  └─┘             └───┘
typ   └─────────────┘  └─┘          └───┘
doc                    └─┘           
534  by congr; funext a; simp
src     └───┘  └──────┘  └────
typ     └───┘  └──────┘  └────
doc            └──────┘  └────
txt     └───┘  └──────┘  └────
par     └───┘  └──────┘  └────
pid                  └┘      
st     └──────────────────────
535  
src  
typ  
doc  
txt  
par  
pid  
st   
536  theorem eval₂_eq_eval_map (g : σ → β) (p : mv_polynomial σ α) :
id                                            └───────────┘  
src                                             └───────────┘
typ                                           └───────────┘  
doc                                             └───────────┘
537    p.eval₂ f g = (map f p).eval g :=
id     └────┘     └─┘   └──┘  
src     └────┘       └─┘     └──┘
typ    └────┘     └─┘   └──┘  
doc     └────┘        └─┘     └──┘
538  begin
st   └─────
539    unfold map eval,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
540    rw eval₂_comp_left (eval₂ id g),
id        └─────────────┘  └───┘ └┘ 
src    └─┘└─────────────┘ └───┘└┘ 
typ    └─┘└─────────────┘ └───┘└┘
doc    └─┘                └───┘   
txt    └─┘                        
par    └─┘                        
pid                              
st   ────────────────────────────────┘└─
541    congr; funext a; simp
src    └───┘  └──────┘  └───┘
typ    └───┘  └──────┘  └───┘
doc           └──────┘  └───┘
txt    └───┘  └──────┘  └───┘
par    └───┘  └──────┘  └───┘
pid                 └┘      
st   ───────────────────────┘
542  end
st   └─┘
543  
544  lemma eval₂_comp_right {γ} [comm_semiring γ]
id                               └───────────┘ 
src                              └───────────┘
typ                              └───────────┘ 
545    (k : β → γ) [is_semiring_hom k]
id                └─────────────┘ 
src                 └─────────────┘
typ               └─────────────┘ 
doc                 └─────────────┘
546    (f : α → β) [is_semiring_hom f] (g : σ → β)
id                └─────────────┘           
src                 └─────────────┘
typ               └─────────────┘           
doc                 └─────────────┘
547    (p) : k (eval₂ f g p) = eval₂ k (k ∘ g) (map f p) :=
id             └───┘      └───┘        └─┘  
src             └───┘         └───┘           └─┘
typ            └───┘      └───┘        └─┘  
doc             └───┘          └───┘            └─┘
548  begin
st   └─────
549    apply mv_polynomial.induction_on p,
id           └────────────────────────┘ 
src    └────┘└────────────────────────┘
typ    └────┘└────────────────────────┘
doc    └────┘                          
txt    └────┘                          
par    └────┘                          
pid                                   
st   ───────────────────────────────────┘└─
550    { intro r, rw [eval₂_C, map_C, eval₂_C] },
id                    └─────┘  └───┘  └─────┘
src      └─────┘  └──┘└─────┘└┘└───┘└┘└─────┘└┘
typ      └─────┘  └──┘└─────┘└┘└───┘└┘└─────┘└┘
doc      └─────┘  └──┘       └┘     └┘       └┘
txt      └─────┘  └──┘       └┘     └┘       └┘
par      └─────┘  └──┘       └┘     └┘       └┘
pid           └┘    └┘       └┘     └┘       
st   ───┘└─────┘└───────────┘└─────┘└───────┘└┘
551    { intros p q hp hq, rw [eval₂_add, is_semiring_hom.map_add k, map_add, eval₂_add, hp, hq] },
id                             └───────┘  └─────────────────────┘   └─────┘  └───────┘  └┘  └┘
src      └──────────────┘  └──┘└───────┘└┘└─────────────────────┘ └┘└─────┘└┘└───────┘└┘  └┘  └┘
typ      └──────────────┘  └──┘└───────┘└┘└─────────────────────┘└┘└─────┘└┘└───────┘└┘└┘└┘└┘└┘
doc      └──────────────┘  └──┘         └┘                        └┘       └┘         └┘  └┘  └┘
txt      └──────────────┘  └──┘         └┘                        └┘       └┘         └┘  └┘  └┘
par      └──────────────┘  └──┘         └┘                        └┘       └┘         └┘  └┘  └┘
pid            └────────┘    └┘         └┘                        └┘       └┘         └┘  └┘  
st   ───┘└──────────────┘└─────────────┘└─────────────────────────┘└───────┘└─────────┘└──┘└──┘└┘
552    { intros p s hp,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid            └─────┘
st   ────────────────┘└─
553      rw [eval₂_mul, is_semiring_hom.map_mul k, map_mul, eval₂_mul, map_X, hp, eval₂_X, eval₂_X] }
id           └───────┘  └─────────────────────┘   └─────┘  └───────┘  └───┘  └┘  └─────┘  └─────┘
src      └──┘└───────┘└┘└─────────────────────┘ └┘└─────┘└┘└───────┘└┘└───┘└┘  └┘└─────┘└┘└─────┘└┘
typ      └──┘└───────┘└┘└─────────────────────┘└┘└─────┘└┘└───────┘└┘└───┘└┘└┘└┘└─────┘└┘└─────┘└┘
doc      └──┘         └┘                        └┘       └┘         └┘     └┘  └┘       └┘       └┘
txt      └──┘         └┘                        └┘       └┘         └┘     └┘  └┘       └┘       └┘
par      └──┘         └┘                        └┘       └┘         └┘     └┘  └┘       └┘       └┘
pid        └┘         └┘                        └┘       └┘         └┘     └┘  └┘       └┘       
st   ────────────────┘└─────────────────────────┘└───────┘└─────────┘└─────┘└──┘└───────┘└───────┘└─
554  end
st   ──┘
555  
556  lemma map_eval₂ (f : α → β) [is_semiring_hom f] (g : γ → mv_polynomial δ α) (p : mv_polynomial γ α) :
id                              └─────────────┘           └───────────┘         └───────────┘  
src                               └─────────────┘             └───────────┘           └───────────┘
typ                             └─────────────┘           └───────────┘         └───────────┘  
doc                               └─────────────┘             └───────────┘           └───────────┘
557    map f (eval₂ C g p) = eval₂ C (map f ∘ g) (map f p) :=
id     └─┘   └───┘      └───┘   └─┘      └─┘  
src    └─┘    └───┘        └───┘   └─┘        └─┘
typ    └─┘   └───┘      └───┘   └─┘      └─┘  
doc    └─┘    └───┘         └───┘   └─┘         └─┘
558  begin
st   └─────
559    apply mv_polynomial.induction_on p,
id           └────────────────────────┘ 
src    └────┘└────────────────────────┘
typ    └────┘└────────────────────────┘
doc    └────┘                          
txt    └────┘                          
par    └────┘                          
pid                                   
st   ───────────────────────────────────┘└─
560    { intro r, rw [eval₂_C, map_C, map_C, eval₂_C] },
id                    └─────┘  └───┘  └───┘  └─────┘
src      └─────┘  └──┘└─────┘└┘└───┘└┘└───┘└┘└─────┘└┘
typ      └─────┘  └──┘└─────┘└┘└───┘└┘└───┘└┘└─────┘└┘
doc      └─────┘  └──┘       └┘     └┘     └┘       └┘
txt      └─────┘  └──┘       └┘     └┘     └┘       └┘
par      └─────┘  └──┘       └┘     └┘     └┘       └┘
pid           └┘    └┘       └┘     └┘     └┘       
st   ───┘└─────┘└───────────┘└─────┘└─────┘└───────┘└┘
561    { intros p q hp hq, rw [eval₂_add, map_add, hp, hq, map_add, eval₂_add] },
id                             └───────┘  └─────┘  └┘  └┘  └─────┘  └───────┘
src      └──────────────┘  └──┘└───────┘└┘└─────┘└┘  └┘  └┘└─────┘└┘└───────┘└┘
typ      └──────────────┘  └──┘└───────┘└┘└─────┘└┘└┘└┘└┘└┘└─────┘└┘└───────┘└┘
doc      └──────────────┘  └──┘         └┘       └┘  └┘  └┘       └┘         └┘
txt      └──────────────┘  └──┘         └┘       └┘  └┘  └┘       └┘         └┘
par      └──────────────┘  └──┘         └┘       └┘  └┘  └┘       └┘         └┘
pid            └────────┘    └┘         └┘       └┘  └┘  └┘       └┘         
st   ───┘└──────────────┘└─────────────┘└───────┘└──┘└──┘└───────┘└─────────┘└┘
562    { intros p s hp,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid            └─────┘
st   ────────────────┘└─
563      rw [eval₂_mul, map_mul, hp, map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X] }
id           └───────┘  └─────┘  └┘  └─────┘  └───┘  └───────┘  └─────┘  └─────┘
src      └──┘└───────┘└┘└─────┘└┘  └┘└─────┘└┘└───┘└┘└───────┘└┘└─────┘└┘└─────┘└┘
typ      └──┘└───────┘└┘└─────┘└┘└┘└┘└─────┘└┘└───┘└┘└───────┘└┘└─────┘└┘└─────┘└┘
doc      └──┘         └┘       └┘  └┘       └┘     └┘         └┘       └┘       └┘
txt      └──┘         └┘       └┘  └┘       └┘     └┘         └┘       └┘       └┘
par      └──┘         └┘       └┘  └┘       └┘     └┘         └┘       └┘       └┘
pid        └┘         └┘       └┘  └┘       └┘     └┘         └┘       └┘       
st   ────────────────┘└───────┘└──┘└───────┘└─────┘└─────────┘└───────┘└───────┘└─
564  end
st   ──┘
565  
566  lemma coeff_map (p : mv_polynomial σ α) : ∀ (m : σ →₀ ℕ), coeff m (p.map f) = f (coeff m p) :=
id                        └───────────┘              └┘    └───┘   └──┘      └───┘  
src                       └───────────┘                 └┘    └───┘     └──┘        └───┘
typ                       └───────────┘              └┘    └───┘   └──┘      └───┘  
doc                       └───────────┘                 └┘     └───┘     └──┘         └───┘
567  begin
st   └─────
568    apply mv_polynomial.induction_on p; clear p,
id           └────────────────────────┘ 
src    └────┘└────────────────────────┘   └─────┘
typ    └────┘└────────────────────────┘  └─────┘
doc    └────┘                             └─────┘
txt    └────┘                             └─────┘
par    └────┘                             └─────┘
pid                                           └┘
st   ────────────────────────────────────────────┘└─
569    { intros r m, rw [map_C], simp only [coeff_C], split_ifs, {refl}, rw is_semiring_hom.map_zero f },
id                       └───┘              └─────┘                         └──────────────────────┘ 
src      └────────┘  └──┘└───┘  └─────────┘└─────┘  └───────┘   └──┘   └─┘└──────────────────────┘ 
typ      └────────┘  └──┘└───┘  └─────────┘└─────┘  └───────┘   └──┘   └─┘└──────────────────────┘
doc      └────────┘  └──┘       └─────────┘         └───────┘   └──┘   └─┘                         
txt      └────────┘  └──┘       └─────────┘         └───────┘   └──┘   └─┘                         
par      └────────┘  └──┘       └─────────┘         └───────┘   └──┘   └─┘                         
pid            └──┘    └┘           └──┘└┘                                                       
st   ───┘└────────┘└─────────┘└────────────────────┘└─────────┘└─────┘└┘└─────────────────────────────┘└┘
570    { intros p q hp hq m, simp only [hp, hq, map_add, coeff_add], rw is_semiring_hom.map_add f },
id                                      └┘  └┘  └─────┘  └───────┘      └─────────────────────┘ 
src      └────────────────┘  └─────────┘  └┘  └┘└─────┘└┘└───────┘  └─┘└─────────────────────┘ 
typ      └────────────────┘  └─────────┘└┘└┘└┘└┘└─────┘└┘└───────┘  └─┘└─────────────────────┘
doc      └────────────────┘  └─────────┘  └┘  └┘       └┘           └─┘                        
txt      └────────────────┘  └─────────┘  └┘  └┘       └┘           └─┘                        
par      └────────────────┘  └─────────┘  └┘  └┘       └┘           └─┘                        
pid            └──────────┘      └──┘└┘  └┘  └┘       └┘                                     
st   ───┘└────────────────┘└──────────────────────────────────────┘└─────────────────────────────┘└┘
571    { intros p i hp m, simp only [hp, map_mul, map_X],
id                                   └┘  └─────┘  └───┘
src      └─────────────┘  └─────────┘  └┘└─────┘└┘└───┘
typ      └─────────────┘  └─────────┘└┘└┘└─────┘└┘└───┘
doc      └─────────────┘  └─────────┘  └┘       └┘     
txt      └─────────────┘  └─────────┘  └┘       └┘     
par      └─────────────┘  └─────────┘  └┘       └┘     
pid            └───────┘      └──┘└┘  └┘       └┘     
st   ──────────────────┘└──────────────────────────────┘└─
572      simp only [hp, mem_support_iff, coeff_mul_X'],
id                  └┘  └─────────────┘  └──────────┘
src      └─────────┘  └┘└─────────────┘└┘└──────────┘
typ      └─────────┘└┘└┘└─────────────┘└┘└──────────┘
doc      └─────────┘  └┘               └┘            
txt      └─────────┘  └┘               └┘            
par      └─────────┘  └┘               └┘            
pid          └──┘└┘  └┘               └┘            
st   ────────────────────────────────────────────────┘└─
573      split_ifs, {refl},
src      └───────┘   └──┘
typ      └───────┘   └──┘
doc      └───────┘   └──┘
txt      └───────┘   └──┘
par      └───────┘   └──┘
st   ────────────┘└─────┘└┘
574      rw is_semiring_hom.map_zero f }
id          └──────────────────────┘ 
src      └─┘└──────────────────────┘ 
typ      └─┘└──────────────────────┘
doc      └─┘                         
txt      └─┘                         
par      └─┘                         
pid                                 
st   ─────────────────────────────────┘└─
575  end
st   ──┘
576  
577  lemma map_injective (hf : function.injective f) :
id                             └────────────────┘ 
src                            └────────────────┘
typ                            └────────────────┘ 
578    function.injective (map f : mv_polynomial σ α → mv_polynomial σ β) :=
id     └────────────────┘  └─┘    └───────────┘     └───────────┘  
src    └────────────────┘  └─┘     └───────────┘       └───────────┘
typ    └────────────────┘  └─┘    └───────────┘     └───────────┘  
doc                        └─┘     └───────────┘       └───────────┘
579  λ p q h, ext _ _ $ λ m, hf $
id         └─┘           └┘
src           └─┘
typ        └─┘           └┘
580  begin
st   └─────
581    rw ← ext_iff at h,
id          └─────┘
src    └───┘└─────┘└───┘
typ    └───┘└─────┘└───┘
doc    └───┘       └───┘
txt    └───┘       └───┘
par    └───┘       └───┘
pid      └─┘       └───┘
st   ──────────────────┘└─
582    specialize h m,
id                 
src    └─────────┘ 
typ    └─────────┘
doc    └─────────┘ 
txt    └─────────┘ 
par    └─────────┘ 
pid               
st   ───────────────┘└─
583    rw [coeff_map, coeff_map] at h,
id         └───────┘  └───────┘
src    └──┘└───────┘└┘└───────┘└────┘
typ    └──┘└───────┘└┘└───────┘└────┘
doc    └──┘         └┘         └────┘
txt    └──┘         └┘         └────┘
par    └──┘         └┘         └────┘
pid      └┘         └┘         └───┘
st   ──────────────┘└─────────┘└───┘└─
584    exact h
id           
src    └────┘ 
typ    └────┘
doc    └────┘ 
txt    └────┘ 
par    └────┘ 
pid          
st   ─────────┘
585  end
st   └─┘
586  
587  end map
588  
589  section degrees
590  
591  section comm_semiring
592  
593  /--
594  The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset.
595  
596  (For example, `degrees (x^2 * y + y^3)` would be `{x, x, y, y, y}`.)
597  -/
598  def degrees (p : mv_polynomial σ α) : multiset σ :=
id                    └───────────┘      └──────┘ 
src                   └───────────┘        └──────┘
typ                   └───────────┘      └──────┘ 
doc                   └───────────┘        └──────┘
599  p.support.sup (λs:σ →₀ ℕ, s.to_multiset)
id   └──────┘└──┘      └┘   └──────────┘
src   └──────┘└──┘       └┘    └──────────┘
typ  └──────┘└──┘      └┘   └──────────┘
doc           └──┘       └┘
600  
601  lemma degrees_monomial (s : σ →₀ ℕ) (a : α) : degrees (monomial s a) ≤ s.to_multiset :=
id                                └┘            └─────┘  └──────┘     └──────────┘
src                                └┘             └─────┘  └──────┘        └──────────┘
typ                               └┘            └─────┘  └──────┘     └──────────┘
doc                                └┘              └─────┘  └──────┘
602  finset.sup_le $ assume t h,
id   └───────────┘           
src  └───────────┘
typ  └───────────┘           
603  begin
st   └─────
604    have := finsupp.support_single_subset h,
id             └───────────────────────────┘ 
src    └──────┘└───────────────────────────┘
typ    └──────┘└───────────────────────────┘
doc    └──────┘                             
txt    └──────┘                             
par    └──────┘                             
pid    └───┘└─┘                             
st   ────────────────────────────────────────┘└─
605    rw [finset.singleton_eq_singleton, finset.mem_singleton] at this,
id         └───────────────────────────┘  └──────────────────┘
src    └──┘└───────────────────────────┘└┘└──────────────────┘└───────┘
typ    └──┘└───────────────────────────┘└┘└──────────────────┘└───────┘
doc    └──┘                             └┘                    └───────┘
txt    └──┘                             └┘                    └───────┘
par    └──┘                             └┘                    └───────┘
pid      └┘                             └┘                    └──────┘
st   ──────────────────────────────────┘└────────────────────┘└──────┘└─
606    rw this
id        └──┘
src    └─┘    
typ    └─┘└──┘
doc    └─┘    
txt    └─┘    
par    └─┘    
pid          
st   ─────────┘
607  end
st   └─┘
608  
609  lemma degrees_monomial_eq (s : σ →₀ ℕ) (a : α) (ha : a ≠ 0) :
id                                   └┘                 
src                                   └┘                   
typ                                  └┘                 
doc                                   └┘
610    degrees (monomial s a) = s.to_multiset :=
id     └─────┘  └──────┘     └──────────┘
src    └─────┘  └──────┘        └──────────┘
typ    └─────┘  └──────┘     └──────────┘
doc    └─────┘  └──────┘
611  le_antisymm (degrees_monomial s a) $ finset.le_sup $
id   └─────────┘  └──────────────┘      └───────────┘
src  └─────────┘  └──────────────┘        └───────────┘
typ  └─────────┘  └──────────────┘      └───────────┘
612    by rw [monomial, finsupp.support_single_ne_zero ha,
id            └──────┘  └────────────────────────────┘ └┘
src       └──┘└──────┘└┘└────────────────────────────┘  └─
typ       └──┘└──────┘└┘└────────────────────────────┘└┘└─
doc       └──┘└──────┘└┘                                └─
txt       └──┘        └┘                                └─
par       └──┘        └┘                                └─
pid         └┘        └┘                                └─
st       └───────────┘└─────────────────────────────────┘└─
613      finset.singleton_eq_singleton, finset.mem_singleton]
id       └───────────────────────────┘  └──────────────────┘
src  ───┘└───────────────────────────┘└┘└──────────────────┘└─
typ  ───┘└───────────────────────────┘└┘└──────────────────┘└─
doc  ───┘                             └┘                    └─
txt  ───┘                             └┘                    └─
par  ───┘                             └┘                    └─
pid  ───┘                             └┘                    
st   ────────────────────────────────┘└────────────────────┘
614  
src  
typ  
doc  
txt  
par  
pid  
st   
615  lemma degrees_C (a : α) : degrees (C a : mv_polynomial σ α) = 0 :=
id                            └─────┘      └───────────┘    
src                            └─────┘       └───────────┘      
typ                           └─────┘      └───────────┘    
doc                            └─────┘       └───────────┘
616  multiset.le_zero.1 $ degrees_monomial _ _
id   └──────────────┘    └──────────────┘
src  └──────────────┘    └──────────────┘
typ  └──────────────┘    └──────────────┘
617  
618  lemma degrees_X (n : σ) : degrees (X n : mv_polynomial σ α) ≤ {n} :=
id                            └─────┘      └───────────┘     
src                            └─────┘       └───────────┘       
typ                           └─────┘      └───────────┘     
doc                            └─────┘       └───────────┘
619  le_trans (degrees_monomial _ _) $ le_of_eq $ to_multiset_single _ _
id   └──────┘  └──────────────┘        └──────┘   └────────────────┘
src  └──────┘  └──────────────┘        └──────┘   └────────────────┘
typ  └──────┘  └──────────────┘        └──────┘   └────────────────┘
620  
621  lemma degrees_zero : degrees (0 : mv_polynomial σ α) = 0 :=
id                        └─────┘      └───────────┘    
src                       └─────┘      └───────────┘      
typ                       └─────┘      └───────────┘    
doc                       └─────┘      └───────────┘
622  by { rw ← C_0, exact degrees_C 0 }
id             └─┘        └───────┘
src       └───┘└─┘  └────┘└───────┘└─┘
typ       └───┘└─┘  └────┘└───────┘└─┘
doc       └───┘     └────┘         └─┘
txt       └───┘     └────┘         └─┘
par       └───┘     └────┘         └─┘
pid         └─┘                   └┘
st     └─────────┘└──────────────────┘└┘
623  
624  lemma degrees_one : degrees (1 : mv_polynomial σ α) = 0 := degrees_C 1
id                       └─────┘      └───────────┘          └───────┘
src                      └─────┘      └───────────┘            └───────┘
typ                      └─────┘      └───────────┘          └───────┘
doc                      └─────┘      └───────────┘
625  
626  lemma degrees_add (p q : mv_polynomial σ α) : (p + q).degrees ≤ p.degrees ⊔ q.degrees :=
id                            └───────────┘          └─────┘   └──────┘  └──────┘
src                           └───────────┘              └─────┘    └──────┘   └──────┘
typ                           └───────────┘          └─────┘   └──────┘  └──────┘
doc                           └───────────┘               └─────┘     └──────┘    └──────┘
627  begin
st   └─────
628    refine finset.sup_le (assume b hb, _),
id            └───────────┘
src    └─────┘└───────────┘       └───────┘
typ    └─────┘└───────────┘       └───────┘
doc    └─────┘                    └───────┘
txt    └─────┘                    └───────┘
par    └─────┘                    └───────┘
pid                              └───────┘
st   ──────────────────────────────────────┘└─
629    have := finsupp.support_add hb, rw finset.mem_union at this,
id             └─────────────────┘ └┘     └──────────────┘
src    └──────┘└─────────────────┘    └─┘└──────────────┘└──────┘
typ    └──────┘└─────────────────┘└┘  └─┘└──────────────┘└──────┘
doc    └──────┘                       └─┘                └──────┘
txt    └──────┘                       └─┘                └──────┘
par    └──────┘                       └─┘                └──────┘
pid    └───┘└─┘                                         └──────┘
st   ───────────────────────────────┘└───────────────────────────┘└┘
630    cases this,
631    { exact le_sup_left_of_le (finset.le_sup this) },
st                                                    └┘
632    { exact le_sup_right_of_le (finset.le_sup this) },
st                                                     └┘
633  end
st   └─┘
634  
635  lemma degrees_sum {ι : Type*} (s : finset ι) (f : ι → mv_polynomial σ α) :
id                                       └┘                            
src                                      └┘
typ                                      └┘                            
doc                                      └┘
636    (s.sum f).degrees ≤ s.sup (λi, (f i).degrees) :=
id                                    
typ                                   
637  begin
638    refine s.induction _ _,
639    { simp only [finset.sum_empty, finset.sup_empty, degrees_zero], exact le_refl _ },
st                                                                                     └┘
640    { assume i s his ih,
641      rw [finset.sup_insert, finset.sum_insert his],
642      exact le_trans (degrees_add _ _) (sup_le_sup_left ih _) }
st                                                               └─
643  end
st   ──┘
644  
645  lemma degrees_mul (p q : mv_polynomial σ α) : (p * q).degrees ≤ p.degrees + q.degrees :=
id                                                                           
typ                                                                          
646  begin
647    refine finset.sup_le (assume b hb, _),
648    have := support_mul p q hb,
id                          
typ                         
649    simp only [finset.mem_bind, finset.singleton_eq_singleton, finset.mem_singleton] at this,
650    rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩,
651    rw [finsupp.to_multiset_add],
652    exact add_le_add (finset.le_sup h₁) (finset.le_sup h₂)
653  end
st   └─┘
654  
655  lemma degrees_prod {ι : Type*} (s : finset ι) (f : ι → mv_polynomial σ α) :
id                                         └┘                            
src                                        └┘
typ                                        └┘                            
doc                                        └┘
656    (s.prod f).degrees ≤ s.sum (λi, (f i).degrees) :=
id                                     
typ                                    
657  begin
658    refine s.induction _ _,
659    { simp only [finset.prod_empty, finset.sum_empty, degrees_one] },
st                                                                    └┘
660    { assume i s his ih,
661      rw [finset.prod_insert his, finset.sum_insert his],
662      exact le_trans (degrees_mul _ _) (add_le_add_left ih _) }
st                                                               └─
663  end
st   ──┘
664  
665  lemma degrees_pow (p : mv_polynomial σ α) :
id                                         
typ                                        
666    ∀(n : ℕ), (p^n).degrees ≤ add_monoid.smul n p.degrees
id                                             
src          
typ                                            
667  | 0       := begin rw [pow_zero, degrees_one], exact multiset.zero_le _ end
st                                                                           └─┘
668  | (n + 1) := le_trans (degrees_mul _ _) (add_le_add_left (degrees_pow n) _)
id      
typ     
669  
670  end comm_semiring
671  
672  end degrees
673  
674  section vars
675  
676  /-- `vars p` is the set of variables appearing in the polynomial `p` -/
677  def vars (p : mv_polynomial σ α) : finset σ := p.degrees.to_finset
id                                      └┘  
src                                       └┘
typ                                     └┘  
doc                                       └┘
678  
679  @[simp] lemma vars_0 : (0 : mv_polynomial σ α).vars = ∅ :=
id                                              
typ                                             
doc    └──┘
680  by rw [vars, degrees_zero, multiset.to_finset_zero]
st                                                     
681  
682  @[simp] lemma vars_monomial (h : a ≠ 0) : (monomial s a).vars = s.support :=
id                                                                
typ                                                               
doc    └──┘
683  by rw [vars, degrees_monomial_eq _ _ h, finsupp.to_finset_to_multiset]
st                                                                        
684  
685  @[simp] lemma vars_C : (C a : mv_polynomial σ α).vars = ∅ :=
id                                               
typ                                              
doc    └──┘
686  by rw [vars, degrees_C, multiset.to_finset_zero]
st                                                  
687  
688  @[simp] lemma vars_X (h : 0 ≠ (1 : α)) : (X n : mv_polynomial σ α).vars = {n} :=
id                                                                          
typ                                                                         
doc    └──┘
689  by rw [X, vars_monomial h.symm, finsupp.support_single_ne_zero zero_ne_one.symm]
st                                                                                  
690  
691  end vars
692  
693  section degree_of
694  
695  /-- `degree_of n p` gives the highest power of X_n that appears in `p` -/
696  def degree_of (n : σ) (p : mv_polynomial σ α) : ℕ := p.degrees.count n
id                                                                   
src                                                  
typ                                                                  
697  
698  end degree_of
699  
700  section total_degree
701  /-- `total_degree p` gives the maximum |s| over the monomials X^s in `p` -/
702  def total_degree (p : mv_polynomial σ α) : ℕ := p.support.sup (λs, s.sum $ λn e, e)
id                                                                             
src                                             
typ                                                                            
703  
704  lemma total_degree_eq (p : mv_polynomial σ α) :
id                                             
typ                                            
705    p.total_degree = p.support.sup (λm, m.to_multiset.card) :=
id                                      
typ                                     
706  begin
707    rw [total_degree],
708    congr, funext m,
709    exact (finsupp.card_to_multiset _).symm
710  end
st   └─┘
711  
712  lemma total_degree_le_degrees_card (p : mv_polynomial σ α) :
id                                                          
typ                                                         
713    p.total_degree ≤ p.degrees.card :=
id                     
typ                    
714  begin
715    rw [total_degree_eq],
716    exact finset.sup_le (assume s hs, multiset.card_le_of_le $ finset.le_sup hs)
id                                 
typ                                
717  end
st   └─┘
718  
719  lemma total_degree_C (a : α) : (C a : mv_polynomial σ α).total_degree = 0 :=
id                                                      
typ                                                     
720  nat.eq_zero_of_le_zero $ finset.sup_le $ assume n hn,
id                                                   
typ                                                  
721    have _ := finsupp.support_single_subset hn,
722    begin
723      rw [finset.singleton_eq_singleton, finset.mem_singleton] at this,
724      subst this,
725      exact le_refl _
726    end
st     └─┘
727  
728  lemma total_degree_zero : (0 : mv_polynomial σ α).total_degree = 0 :=
id                                                 
typ                                                
729  by rw [← C_0]; exact total_degree_C (0 : α)
id                                            
typ                                           
730  
731  lemma total_degree_one : (1 : mv_polynomial σ α).total_degree = 0 :=
id                                                
typ                                               
732  total_degree_C (1 : α)
id                       
typ                      
733  
734  lemma total_degree_add (a b : mv_polynomial σ α) :
id                                                
typ                                               
735    (a + b).total_degree ≤ max a.total_degree b.total_degree :=
id                                             
typ                                            
736  finset.sup_le $ assume n hn,
id                          
typ                         
737    have _ := finsupp.support_add hn,
738    begin
739      rw finset.mem_union at this,
740      cases this,
741      { exact le_max_left_of_le (finset.le_sup this) },
st                                                      └┘
742      { exact le_max_right_of_le (finset.le_sup this) }
st                                                       └┘
743    end
st     └─┘
744  
745  lemma total_degree_mul (a b : mv_polynomial σ α) :
id                                                
typ                                               
746    (a * b).total_degree ≤ a.total_degree + b.total_degree :=
id                                           
typ                                          
747  finset.sup_le $ assume n hn,
id                          
typ                         
748    have _ := finsupp.support_mul a b hn,
id                                   
typ                                  
749    begin
750      simp only [finset.mem_bind, finset.mem_singleton, finset.singleton_eq_singleton] at this,
751      rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩,
752      rw [finsupp.sum_add_index],
753      { exact add_le_add (finset.le_sup h₁) (finset.le_sup h₂) },
st                                                                └┘
754      { assume a, refl },
st                        └┘
755      { assume a b₁ b₂, refl }
st                              └┘
756    end
st     └─┘
757  
758  lemma total_degree_list_prod :
759    ∀(s : list (mv_polynomial σ α)), s.prod.total_degree ≤ (s.map mv_polynomial.total_degree).sum
id                                
typ                               
760  | []        := by rw [@list.prod_nil (mv_polynomial σ α) _, total_degree_one]; refl
id                                                                                  └──┘
src                                                                                 └──┘
typ                                                                                 └──┘
doc                                                                                 └──┘
761  | (p :: ps) :=
762    begin
763      rw [@list.prod_cons (mv_polynomial σ α) _, list.map, list.sum_cons],
id                                           
typ                                          
764      exact le_trans (total_degree_mul _ _) (add_le_add_left (total_degree_list_prod ps) _)
765    end
st     └─┘
766  
767  lemma total_degree_multiset_prod (s : multiset (mv_polynomial σ α)) :
id                                                                  
typ                                                                 
768    s.prod.total_degree ≤ (s.map mv_polynomial.total_degree).sum :=
769  begin
770    refine quotient.induction_on s (assume l, _),
771    rw [multiset.quot_mk_to_coe, multiset.coe_prod, multiset.coe_map, multiset.coe_sum],
772    exact total_degree_list_prod l
773  end
st   └─┘
774  
775  lemma total_degree_finset_prod {ι : Type*}
776    (s : finset ι) (f : ι → mv_polynomial σ α) :
id            └┘                            
src           └┘
typ           └┘                            
doc           └┘
777    (s.prod f).total_degree ≤ s.sum (λi, (f i).total_degree) :=
id                                          
typ                                         
778  begin
779    refine le_trans (total_degree_multiset_prod _) _,
780    rw [multiset.map_map],
781    refl
782  end
st   └─┘
783  
784  end total_degree
785  
786  end comm_semiring
787  
788  section comm_ring
789  variable [comm_ring α]
id             └┘  └──┘
src            └┘  └──┘
typ            └┘  └──┘
790  variables {p q : mv_polynomial σ α}
791  
792  instance : ring (mv_polynomial σ α) := finsupp.ring
id                                   
typ                                  
793  instance : comm_ring (mv_polynomial σ α) := finsupp.comm_ring
id                                        
typ                                       
794  instance : has_scalar α (mv_polynomial σ α) := finsupp.has_scalar
id                                          
typ                                         
795  instance : module α (mv_polynomial σ α) := finsupp.module _ α
id                                                            
typ                                                           
796  
797  instance C.is_ring_hom : is_ring_hom (C : α → mv_polynomial σ α) :=
id                                                               
typ                                                              
798  by apply is_ring_hom.of_semiring
799  
800  variables (σ a a')
801  lemma C_sub : (C (a - a') : mv_polynomial σ α) = C a - C a' := is_ring_hom.map_sub _
id                        └┘                              └┘
typ                       └┘                              └┘
802  
803  @[simp] lemma C_neg : (C (-a) : mv_polynomial σ α) = -C a := is_ring_hom.map_neg _
id                                                        
typ                                                       
doc    └──┘
804  
805  @[simp] lemma coeff_sub (m : σ →₀ ℕ) (p q : mv_polynomial σ α) :
id                                                            
src                                    
typ                                                           
doc    └──┘
806    coeff m (p - q) = coeff m p - coeff m q := finsupp.sub_apply
id                                       
typ                                      
807  
808  instance coeff.is_add_group_hom (m : σ →₀ ℕ) :
id                                            
src                                            
typ                                           
809    is_add_group_hom (coeff m : mv_polynomial σ α → α) :=
id                                                  
typ                                                 
810  { map_add := coeff_add m }
id                          
typ                         
811  
812  variables {σ} (p)
813  theorem C_mul' : mv_polynomial.C a * p = a • p :=
id                                           
typ                                          
814  begin
815    apply finsupp.induction p,
816    { exact (mul_zero $ mv_polynomial.C a).trans (@smul_zero α (mv_polynomial σ α) _ _ _ a).symm },
id                                                                                        
typ                                                                                       
st                                                                                                  └┘
817    intros p b f haf hb0 ih,
818    rw [mul_add, ih, @smul_add α (mv_polynomial σ α) _ _ _ a], congr' 1,
id                                                          
typ                                                         
819    rw [finsupp.mul_def, finsupp.smul_single, mv_polynomial.C, mv_polynomial.monomial],
820    rw [finsupp.sum_single_index, finsupp.sum_single_index, zero_add, smul_eq_mul],
821    { rw [mul_zero, finsupp.single_zero] },
st                                         └┘
822    { rw finsupp.sum_single_index,
823      all_goals { rw [zero_mul, finsupp.single_zero] } }
st                                                     └───
824  end
st   ──┘
825  
826  lemma smul_eq_C_mul (p : mv_polynomial σ α) (a : α) : a • p = C a * p :=
id                                                               
typ                                                              
827  begin
828    rw [← finsupp.sum_single p, @finsupp.smul_sum (σ →₀ ℕ) α α, finsupp.mul_sum],
829    refine finset.sum_congr rfl (assume n _, _),
id                                         
typ                                        
830    simp only [finsupp.smul_single],
831    exact C_mul_monomial.symm
832  end
st   └─┘
833  
834  @[simp] lemma smul_eval (x) (p : mv_polynomial σ α) (s) : (s • p).eval x = s * p.eval x :=
id                                                                                    
typ                                                                                   
doc    └──┘
835  by rw [smul_eq_C_mul, eval_mul, eval_C]
st                                         
836  
837  section degrees
838  
839  lemma degrees_neg (p : mv_polynomial σ α) : (- p).degrees = p.degrees :=
id                                         
typ                                        
840  by rw [degrees, finsupp.support_neg]; refl
id                                         └──┘
src                                        └──┘
typ                                        └──┘
doc                                        └──┘
841  
842  lemma degrees_sub (p q : mv_polynomial σ α) :
id                                           
typ                                          
843    (p - q).degrees ≤ p.degrees ⊔ q.degrees :=
844  le_trans (degrees_add p (-q)) $ by rw [degrees_neg]
845  
846  end degrees
847  
848  section eval₂
849  
850  variables [comm_ring β]
id              └──┘  └─┘
src             └──┘  └─┘
typ             └──┘  └─┘
851  variables (f : α → β) [is_ring_hom f] (g : σ → β)
852  
853  instance eval₂.is_ring_hom : is_ring_hom (eval₂ f g) :=
id                                                    
typ                                                   
854  by apply is_ring_hom.of_semiring
855  
856  lemma eval₂_sub : (p - q).eval₂ f g = p.eval₂ f g - q.eval₂ f g := is_ring_hom.map_sub _
id                                                            
typ                                                           
857  
858  @[simp] lemma eval₂_neg : (-p).eval₂ f g = -(p.eval₂ f g) := is_ring_hom.map_neg _
id                                                       
typ                                                      
doc    └──┘
859  
860  lemma hom_C (f : mv_polynomial σ ℤ → β) [is_ring_hom f] (n : ℤ) : f (C n) = (n : β) :=
id                                                                              
src                                                              
typ                                                                             
861  congr_fun (int.eq_cast' (f ∘ C)) n
id                                    
typ                                   
862  
863  /-- A ring homomorphism f : Z[X_1, X_2, ...] → R
864  is determined by the evaluations f(X_1), f(X_2), ... -/
865  @[simp] lemma eval₂_hom_X {α : Type u} (c : ℤ → β) [is_ring_hom c]
id                                                                 
src                                              
typ                                                                
doc    └──┘
866    (f : mv_polynomial α ℤ → β) [is_ring_hom f] (x : mv_polynomial α ℤ) :
id                                                                  
src                                                                    
typ                                                                 
867    eval₂ c (f ∘ X) x = f x :=
id                          
typ                         
868  mv_polynomial.induction_on x
id                              
typ                             
869  (λ n, by { rw [hom_C f, eval₂_C, int.eq_cast' c], refl })
id                                                
typ                                               
st                                                          └┘
870  (λ p q hp hq, by { rw [eval₂_add, hp, hq], exact (is_ring_hom.map_add f).symm })
id       
typ      
st                                                                                 └┘
871  (λ p n hp, by { rw [eval₂_mul, eval₂_X, hp], exact (is_ring_hom.map_mul f).symm })
id       
typ      
st                                                                                   └┘
872  
873  /-- Ring homomorphisms out of integer polynomials on a type `σ` are the same as
874  functions out of the type `σ`, -/
875  def hom_equiv : (mv_polynomial σ ℤ →+* β) ≃ (σ → β) :=
id                                                
src                                   
typ                                               
876  { to_fun := λ f, ⇑f ∘ X,
877    inv_fun := λ f, ring_hom.of (eval₂ (λ n : ℤ, (n : β)) f),
id                                                       
src                                              
typ                                                      
878    left_inv := λ f, ring_hom.ext  $ eval₂_hom_X _ _,
879    right_inv := λ f, funext $ λ x, by simp only [ring_hom.coe_of, function.comp_app, eval₂_X] }
id                                 
typ                                
880  
881  end eval₂
882  
883  section eval
884  
885  variables (f : σ → α)
886  
887  instance eval.is_ring_hom : is_ring_hom (eval f) := eval₂.is_ring_hom _ _
id                                                 
typ                                                
888  
889  lemma eval_sub : (p - q).eval f = p.eval f - q.eval f := is_ring_hom.map_sub _
id                                                     
typ                                                    
890  
891  @[simp] lemma eval_neg : (-p).eval f = -(p.eval f) := is_ring_hom.map_neg _
id                                                  
typ                                                 
doc    └──┘
892  
893  end eval
894  
895  section map
896  
897  variables [comm_ring β]
id               └┘ └┘ 
src              └┘ └┘ 
typ              └┘ └┘ 
898  variables (f : α → β) [is_ring_hom f]
899  
900  instance map.is_ring_hom : is_ring_hom (map f : mv_polynomial σ α → mv_polynomial σ β) :=
id                                                                                   
typ                                                                                  
901  eval₂.is_ring_hom _ _
902  
903  lemma map_sub : (p - q).map f = p.map f - q.map f := is_ring_hom.map_sub _
id                                                 
typ                                                
904  
905  @[simp] lemma map_neg : (-p).map f = -(p.map f) := is_ring_hom.map_neg _
id                                               
typ                                              
doc    └──┘
906  
907  end map
908  
909  end comm_ring
910  
911  section rename
912  variables {α} [comm_semiring α]
id                   └──┘  └──┘
src                  └──┘  └──┘
typ                  └──┘  └──┘
913  
914  /-- Rename all the variables in a multivariable polynomial. -/
915  def rename (f : β → γ) : mv_polynomial β α → mv_polynomial γ α :=
id                                                           
typ                                                          
916  eval₂ C (X ∘ f)
id                
typ               
917  
918  instance rename.is_semiring_hom (f : β → γ) :
id                                           
typ                                          
919    is_semiring_hom (rename f : mv_polynomial β α → mv_polynomial γ α) :=
id                                                                 
typ                                                                
920  by unfold rename; apply_instance
id                     └────────────┘
src                    └────────────┘
typ                    └────────────┘
doc                    └────────────┘
921  
922  @[simp] lemma rename_C (f : β → γ) (a : α) : rename f (C a) = C a :=
id                                                              
typ                                                             
doc    └──┘
923  eval₂_C _ _ _
924  
925  @[simp] lemma rename_X (f : β → γ) (b : β) : rename f (X b : mv_polynomial β α) = X (f b) :=
id                                                                                   
typ                                                                                  
doc    └──┘
926  eval₂_X _ _ _
927  
928  @[simp] lemma rename_zero (f : β → γ) :
id                                     
typ                                    
doc    └──┘
929    rename f (0 : mv_polynomial β α) = 0 :=
id                                 
typ                                
930  eval₂_zero _ _
931  
932  @[simp] lemma rename_one (f : β → γ) :
id                                     
typ                                    
doc    └──┘
933    rename f (1 : mv_polynomial β α) = 1 :=
id                                 
typ                                
934  eval₂_one _ _
935  
936  @[simp] lemma rename_add (f : β → γ) (p q : mv_polynomial β α) :
id                                                             
typ                                                            
doc    └──┘
937    rename f (p + q) = rename f p + rename f q :=
id                                        
typ                                       
938  eval₂_add _ _
939  
940  @[simp] lemma rename_sub {α} [comm_ring α]
id                                  └┘ └┘  
src                                 └┘ └┘ 
typ                                 └┘ └┘  
doc    └──┘
941    (f : β → γ) (p q : mv_polynomial β α) :
id                                      
typ                                     
942    rename f (p - q) = rename f p - rename f q :=
id                                          
typ                                         
943  eval₂_sub _ _ _
944  
945  @[simp] lemma rename_mul (f : β → γ) (p q : mv_polynomial β α) :
id                                                            
typ                                                           
doc    └──┘
946    rename f (p * q) = rename f p * rename f q :=
id                                        
typ                                       
947  eval₂_mul _ _
948  
949  @[simp] lemma rename_pow (f : β → γ) (p : mv_polynomial β α) (n : ℕ) :
id                                                                 
src                                                                    
typ                                                                
doc    └──┘
950    rename f (p^n) = (rename f p)^n :=
id                               
typ                              
951  eval₂_pow _ _
952  
953  lemma map_rename [comm_semiring β] (f : α → β) [is_semiring_hom f]
id                      └┘ └┘ └┘ └┘                              
src                     └┘ └┘ └┘ └┘
typ                     └┘ └┘ └┘ └┘                              
954    (g : γ → δ) (p : mv_polynomial γ α) :
id                                   
typ                                  
955    map f (rename g p) = rename g (map f p) :=
id                                     
typ                                    
956  mv_polynomial.induction_on p
id                              
typ                             
957    (λ a, by simp)
id        
typ       
958    (λ p q hp hq, by simp [hp, hq])
id         
typ        
959    (λ p n hp, by simp [hp])
id         
typ        
960  
961  @[simp] lemma rename_rename (f : β → γ) (g : γ → δ) (p : mv_polynomial β α) :
id                                                                       
typ                                                                      
doc    └──┘
962    rename g (rename f p) = rename (g ∘ f) p :=
id                                      
typ                                     
963  show rename g (eval₂ C (X ∘ f) p) = _,
id                              
typ                             
964    by simp only [eval₂_comp_left (rename g) C (X ∘ f) p, (∘), rename_C, rename_X]; refl
id                                                                                  └──┘
src                                                                                    └──┘
typ                                                                                 └──┘
doc                                                                                    └──┘
965  
966  @[simp] lemma rename_id (p : mv_polynomial β α) : rename id p = p :=
id                                                                
typ                                                               
doc    └──┘
967  eval₂_eta p
id             
typ            
968  
969  lemma rename_monomial (f : β → γ) (p : β →₀ ℕ) (a : α) :
id                                                   
src                                              
typ                                                  
970    rename f (monomial p a) = monomial (p.map_domain f) a :=
id                                                    
typ                                                   
971  begin
972    rw [rename, eval₂_monomial, monomial_eq, finsupp.prod_map_domain_index],
973    { exact assume n, pow_zero _ },
id                    
typ                   
st                                  └┘
974    { exact assume n i₁ i₂, pow_add _ _ _ }
id                     └┘ └┘
typ                    └┘ └┘
st                                           └─
975  end
st   ──┘
976  
977  lemma rename_eq (f : β → γ) (p : mv_polynomial β α) :
id                                                 
typ                                                
978    rename f p = finsupp.map_domain (finsupp.map_domain f) p :=
id                                                          
typ                                                         
979  begin
980    simp only [rename, eval₂, finsupp.map_domain],
981    congr, ext s a : 2,
982    rw [← monomial, monomial_eq, finsupp.prod_sum_index],
983    congr, ext n i : 2,
984    rw [finsupp.prod_single_index],
985    exact pow_zero _,
986    exact assume a, pow_zero _,
id                  
typ                 
987    exact assume a b c, pow_add _ _ _
id                    
typ                   
988  end
st   └─┘
989  
990  lemma injective_rename (f : β → γ) (hf : function.injective f) :
id                                                             
typ                                                            
991    function.injective (rename f : mv_polynomial β α → mv_polynomial γ α) :=
id                                                                    
typ                                                                   
992  have (rename f : mv_polynomial β α → mv_polynomial γ α) =
id                                                    
typ                                                   
993    finsupp.map_domain (finsupp.map_domain f) := funext (rename_eq f),
id                                                                   
typ                                                                  
994  begin
995    rw this,
996    exact finsupp.injective_map_domain (finsupp.injective_map_domain hf)
id                                                                      └┘
typ                                                                     └┘
997  end
st   └─┘
998  
999  lemma total_degree_rename_le (f : β → γ) (p : mv_polynomial β α) :
id                                                              
typ                                                             
1000    (p.rename f).total_degree ≤ p.total_degree :=
id                                
typ                               
1001  finset.sup_le $ assume b,
1002    begin
1003      assume h,
1004      rw rename_eq at h,
1005      have h' := finsupp.map_domain_support h,
1006      rw finset.mem_image at h',
1007      rcases h' with ⟨s, hs, rfl⟩,
1008      rw finsupp.sum_map_domain_index,
1009      exact le_trans (le_refl _) (finset.le_sup hs),
1010      exact assume _, rfl,
id                    
typ                   
1011      exact assume _ _ _, rfl
id                      
typ                     
1012    end
st     └─┘
1013  
1014  section
1015  variables [comm_semiring β] (f : α → β) [is_semiring_hom f]
id              └──┘  └──┘  
src             └──┘  └──┘  
typ             └──┘  └──┘  
1016  variables (k : γ → δ) (g : δ → β) (p : mv_polynomial γ α)
1017  
1018  lemma eval₂_rename : (p.rename k).eval₂ f g = p.eval₂ f (g ∘ k) :=
id                                                         
typ                                                        
1019  by apply mv_polynomial.induction_on p; { intros, simp [*] }
st                                                             └┘
1020  
1021  lemma rename_eval₂ (g : δ → mv_polynomial γ α) :
id                                             
typ                                            
1022    (p.eval₂ C (g ∘ k)).rename k = (p.rename k).eval₂ C (rename k ∘ g) :=
id                                                             
typ                                                            
1023  by apply mv_polynomial.induction_on p; { intros, simp [*] }
st                                                             └┘
1024  
1025  lemma rename_prodmk_eval₂ (d : δ) (g : γ → mv_polynomial γ α) :
id                                                           
typ                                                          
1026    (p.eval₂ C g).rename (prod.mk d) = p.eval₂ C (λ x, (g x).rename (prod.mk d)) :=
id                                                                          
typ                                                                         
1027  by apply mv_polynomial.induction_on p; { intros, simp [*] }
st                                                             └┘
1028  
1029  lemma eval₂_rename_prodmk (g : δ × γ → β) (d : δ) :
id                                               
typ                                              
1030    (rename (prod.mk d) p).eval₂ f g = eval₂ f (λ i, g (d, i)) p :=
id                                                      
typ                                                     
1031  by apply mv_polynomial.induction_on p; { intros, simp [*] }
st                                                             └┘
1032  
1033  lemma eval_rename_prodmk (g : δ × γ → α) (d : δ) :
id                                              
typ                                             
1034    (rename (prod.mk d) p).eval g = eval (λ i, g (d, i)) p :=
id                                                 
typ                                                
1035  eval₂_rename_prodmk id _ _ _
1036  
1037  end
1038  
1039  end rename
1040  
1041  lemma eval₂_cast_comp {β : Type u} {γ : Type v} (f : γ → β)
id                                                           
typ                                                          
1042    {α : Type w} [comm_ring α] (c : ℤ → α) [is_ring_hom c] (g : β → α) (x : mv_polynomial γ ℤ) :
id                     └──┘                                                            
src                    └──┘                                                                  
typ                    └──┘                                                            
1043    eval₂ c (g ∘ f) x = eval₂ c g (rename f x) :=
id                                      
typ                                     
1044  mv_polynomial.induction_on x
id                              
typ                             
1045  (λ n, by simp only [eval₂_C, rename_C])
id      
typ     
1046  (λ p q hp hq, by simp only [hp, hq, rename, eval₂_add])
id       
typ      
1047  (λ p n hp, by simp only [hp, rename, eval₂_X, eval₂_mul])
id       
typ      
1048  
1049  instance rename.is_ring_hom
1050    {α} [comm_ring α] (f : β → γ) :
id          └──┘  └─┘            
src         └──┘  └─┘
typ         └──┘  └─┘            
1051    is_ring_hom (rename f : mv_polynomial β α → mv_polynomial γ α) :=
id                                                             
typ                                                            
1052  @is_ring_hom.of_semiring (mv_polynomial β α) (mv_polynomial γ α) _ _ (rename f)
id                                                                            
typ                                                                           
1053    (rename.is_semiring_hom f)
id                             
typ                            
1054  
1055  section equiv
1056  
1057  variables (α) [comm_semiring α]
id                   └┘ └┘ └┘ └┘
src                  └┘ └┘ └┘ └┘
typ                  └┘ └┘ └┘ └┘
1058  
1059  /-- The ring isomorphism between multivariable polynomials in no variables and the ground ring. -/
1060  def pempty_ring_equiv : mv_polynomial pempty α ≃+* α :=
id                                         └────┘      
src                                        └────┘
typ                                        └────┘      
doc                                        └────┘
1061  { to_fun    := mv_polynomial.eval₂ id $ pempty.elim,
1062    inv_fun   := C,
1063    left_inv  := is_id _ (by apply_instance) (assume a, by rw [eval₂_C]; refl) (assume a, a.elim),
id                                                                         └──┘            
src                                                                         └──┘
typ                                                                        └──┘            
doc                                                                         └──┘
1064    right_inv := λ r, eval₂_C _ _ _,
id                    
typ                   
1065    map_mul'  := λ _ _, eval₂_mul _ _,
id                     
typ                    
1066    map_add'  := λ _ _, eval₂_add _ _ }
id                      
typ                     
1067  
1068  /--
1069  The ring isomorphism between multivariable polynomials in a single variable and
1070  polynomials over the ground ring.
1071  -/
1072  def punit_ring_equiv : mv_polynomial punit α ≃+* polynomial α :=
id                                        └───┘                 
src                                       └───┘
typ                                       └───┘                 
1073  { to_fun    := eval₂ polynomial.C (λu:punit, polynomial.X),
id                                         └──┘
src                                        └──┘
typ                                        └──┘
1074    inv_fun   := polynomial.eval₂ mv_polynomial.C (X punit.star),
id                                                      └──┘  └──┘
src                                                     └──┘  └──┘
typ                                                     └──┘  └──┘
1075    left_inv  :=
1076      begin
1077        refine is_id _ _ _ _,
1078        apply is_semiring_hom.comp (eval₂ polynomial.C (λu:punit, polynomial.X)) _; apply_instance,
id                                                            └───┘                    └────────────┘
src                                                           └───┘                    └────────────┘
typ                                                           └───┘                    └────────────┘
doc                                                                                    └────────────┘
1079        { assume a, rw [eval₂_C, polynomial.eval₂_C] },
st                                                     └┘
1080        { rintros ⟨⟩, rw [eval₂_X, polynomial.eval₂_X] }
st                                                       └┘
1081      end,
st       └─┘
1082    right_inv := assume p, polynomial.induction_on p
id                                                   
typ                                                  
1083      (assume a, by rw [polynomial.eval₂_C, mv_polynomial.eval₂_C])
id               
typ              
st                                                                  
1084      (assume p q hp hq, by rw [polynomial.eval₂_add, mv_polynomial.eval₂_add, hp, hq])
id                
typ               
st                                                                                      
1085      (assume p n hp,
id                
typ               
1086        by rw [polynomial.eval₂_mul, polynomial.eval₂_pow, polynomial.eval₂_X, polynomial.eval₂_C,
1087          eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]),
st                                                 
1088    map_mul'  := λ _ _, eval₂_mul _ _,
id                     
typ                    
1089    map_add'  := λ _ _, eval₂_add _ _ }
id                     
typ                    
1090  
1091  /-- The ring isomorphism between multivariable polynomials induced by an equivalence of the variables.  -/
1092  def ring_equiv_of_equiv (e : β ≃ γ) : mv_polynomial β α ≃+* mv_polynomial γ α :=
id                                                                          
typ                                                                         
1093  { to_fun    := rename e,
id                         
typ                        
1094    inv_fun   := rename e.symm,
id                         
typ                        
1095    left_inv  := λ p, by simp only [rename_rename, (∘), e.symm_apply_apply]; exact rename_id p,
id                                                                                              
typ                                                                                             
1096    right_inv := λ p, by simp only [rename_rename, (∘), e.apply_symm_apply]; exact rename_id p,
id                                                                                             
typ                                                                                            
1097    map_mul'  := rename_mul e,
id                             
typ                            
1098    map_add'  := rename_add e }
id                             
typ                            
1099  
1100  /-- The ring isomorphism between multivariable polynomials induced by a ring isomorphism of the ground ring. -/
1101  def ring_equiv_congr [comm_semiring γ] (e : α ≃+* γ) : mv_polynomial β α ≃+* mv_polynomial β γ :=
id                         └┘  └──┘  └─┘                                                     
src                        └┘  └──┘  └─┘
typ                        └┘  └──┘  └─┘                                                     
1102  { to_fun    := map e,
1103    inv_fun   := map e.symm,
1104    left_inv  := assume p,
1105      have (e.symm ∘ e) = id,
1106      { ext a, exact e.symm_apply_apply a },
id                                         
typ                                        
st                                           └┘
1107      by simp only [map_map, this, map_id],
1108    right_inv := assume p,
id                         
typ                        
1109      have (e ∘ e.symm) = id,
1110      { ext a, exact e.apply_symm_apply a },
id                                         
typ                                        
st                                           └┘
1111      by simp only [map_map, this, map_id],
1112    map_mul'  := map_mul _,
1113    map_add'  := map_add _ }
1114  
1115  section
1116  variables (β γ δ)
1117  
1118  /--
1119  The function from multivariable polynomials in a sum of two types,
1120  to multivariable polynomials in one of the types,
1121  with coefficents in multivariable polynomials in the other type.
1122  
1123  See `sum_ring_equiv` for the ring isomorphism.
1124  -/
1125  def sum_to_iter : mv_polynomial (β ⊕ γ) α → mv_polynomial β (mv_polynomial γ α) :=
id                                                                           
typ                                                                          
1126  eval₂ (C ∘ C) (λbc, sum.rec_on bc X (C ∘ X))
id                   └┘             └┘
typ                  └┘             └┘
1127  
1128  instance is_semiring_hom_C_C :
1129    is_semiring_hom (C ∘ C : α → mv_polynomial β (mv_polynomial γ α)) :=
id                                                                
typ                                                               
1130  @is_semiring_hom.comp _ _ _ _ C mv_polynomial.is_semiring_hom _ _ C mv_polynomial.is_semiring_hom
1131  
1132  instance is_semiring_hom_sum_to_iter : is_semiring_hom (sum_to_iter α β γ) :=
id                                                                         
typ                                                                        
1133  eval₂.is_semiring_hom _ _
1134  
1135  lemma sum_to_iter_C (a : α) : sum_to_iter α β γ (C a) = C (C a) :=
id                                                           
typ                                                          
1136  eval₂_C _ _ a
id               
typ              
1137  
1138  lemma sum_to_iter_Xl (b : β) : sum_to_iter α β γ (X (sum.inl b)) = X b :=
id                                                                    
typ                                                                   
1139  eval₂_X _ _ (sum.inl b)
id                        
typ                       
1140  
1141  lemma sum_to_iter_Xr (c : γ) : sum_to_iter α β γ (X (sum.inr c)) = C (X c) :=
id                                                                       
typ                                                                      
1142  eval₂_X _ _ (sum.inr c)
id                        
typ                       
1143  
1144  /--
1145  The function from multivariable polynomials in one type,
1146  with coefficents in multivariable polynomials in another type,
1147  to multivariable polynomials in the sum of the two types.
1148  
1149  See `sum_ring_equiv` for the ring isomorphism.
1150  -/
1151  def iter_to_sum : mv_polynomial β (mv_polynomial γ α) → mv_polynomial (β ⊕ γ) α :=
id                                                                            
typ                                                                           
1152  eval₂ (eval₂ C (X ∘ sum.inr)) (X ∘ sum.inl)
1153  
1154  instance is_semiring_hom_iter_to_sum : is_semiring_hom (iter_to_sum α β γ) :=
id                                                                         
typ                                                                        
1155  eval₂.is_semiring_hom _ _
1156  
1157  lemma iter_to_sum_C_C (a : α) : iter_to_sum α β γ (C (C a)) = C a :=
id                                                              
typ                                                             
1158  eq.trans (eval₂_C _ _ (C a)) (eval₂_C _ _ _)
id                            
typ                           
1159  
1160  lemma iter_to_sum_X (b : β) : iter_to_sum α β γ (X b) = X (sum.inl b) :=
id                                                                 
typ                                                                
1161  eval₂_X _ _ _
1162  
1163  lemma iter_to_sum_C_X (c : γ) : iter_to_sum α β γ (C (X c)) = X (sum.inr c) :=
id                                                                       
typ                                                                      
1164  eq.trans (eval₂_C _ _ (X c)) (eval₂_X _ _ _)
id                            
typ                           
1165  
1166  /-- A helper function for `sum_ring_equiv`. -/
1167  def mv_polynomial_equiv_mv_polynomial [comm_semiring δ]
id                                            └──┘  └──┘ 
src                                           └──┘  └──┘
typ                                           └──┘  └──┘ 
1168    (f : mv_polynomial β α → mv_polynomial γ δ) (hf : is_semiring_hom f)
id                                           
typ                                          
1169    (g : mv_polynomial γ δ → mv_polynomial β α) (hg : is_semiring_hom g)
id                                           
typ                                          
1170    (hfgC : ∀a, f (g (C a)) = C a)
id                               
typ                              
1171    (hfgX : ∀n, f (g (X n)) = X n)
id                               
typ                              
1172    (hgfC : ∀a, g (f (C a)) = C a)
id                               
typ                              
1173    (hgfX : ∀n, g (f (X n)) = X n) :
id                               
typ                              
1174    mv_polynomial β α ≃+* mv_polynomial γ δ :=
id                                        
typ                                       
1175  { to_fun    := f, inv_fun := g,
1176    left_inv  := is_id _ (is_semiring_hom.comp _ _) hgfC hgfX,
1177    right_inv := is_id _ (is_semiring_hom.comp _ _) hfgC hfgX,
1178    map_mul'  := hf.map_mul,
1179    map_add'  := hf.map_add }
1180  
1181  /--
1182  The ring isomorphism between multivariable polynomials in a sum of two types,
1183  and multivariable polynomials in one of the types,
1184  with coefficents in multivariable polynomials in the other type.
1185  -/
1186  def sum_ring_equiv : mv_polynomial (β ⊕ γ) α ≃+* mv_polynomial β (mv_polynomial γ α) :=
id                                                                                
typ                                                                               
1187  begin
1188    apply @mv_polynomial_equiv_mv_polynomial α (β ⊕ γ) _ _ _ _
1189      (sum_to_iter α β γ) _ (iter_to_sum α β γ) _,
1190    { assume p,
1191      apply hom_eq_hom _ _ _ _ _ _ p,
id                                    
typ                                   
1192      apply_instance,
1193      { apply @is_semiring_hom.comp _ _ _ _ _ _ _ _ _ _,
1194        apply_instance,
1195        apply @is_semiring_hom.comp _ _ _ _ _ _ _ _ _ _,
1196        apply_instance,
1197        { apply @mv_polynomial.is_semiring_hom },
st                                                └┘
1198        { apply mv_polynomial.is_semiring_hom_iter_to_sum α β γ },
id                                                             
typ                                                            
st                                                                 └┘
1199        { apply mv_polynomial.is_semiring_hom_sum_to_iter α β γ } },
id                                                             
typ                                                            
st                                                                 └──┘
1200      { apply mv_polynomial.is_semiring_hom },
st                                             └┘
1201      { assume a, rw [iter_to_sum_C_C α β γ, sum_to_iter_C α β γ] },
id                                                           
typ                                                          
st                                                                  └┘
1202      { assume c, rw [iter_to_sum_C_X α β γ, sum_to_iter_Xr α β γ] } },
id                                                            
typ                                                           
st                                                                   └──┘
1203    { assume b, rw [iter_to_sum_X α β γ, sum_to_iter_Xl α β γ] },
id                                                        
typ                                                       
st                                                               └┘
1204    { assume a, rw [sum_to_iter_C α β γ, iter_to_sum_C_C α β γ] },
id                                                         
typ                                                        
st                                                                └┘
1205    { assume n, cases n with b c,
id                       
typ                      
1206      { rw [sum_to_iter_Xl, iter_to_sum_X] },
st                                           └┘
1207      { rw [sum_to_iter_Xr, iter_to_sum_C_X] } },
st                                             └──┘
1208    { apply mv_polynomial.is_semiring_hom_sum_to_iter α β γ },
id                                                         
typ                                                        
st                                                             └┘
1209    { apply mv_polynomial.is_semiring_hom_iter_to_sum α β γ }
id                                                         
typ                                                        
st                                                             └─
1210  end
st   ──┘
1211  
1212  /--
1213  The ring isomorphism between multivariable polynomials in `option β` and
1214  polynomials with coefficients in `mv_polynomial β α`.
1215  -/
1216  def option_equiv_left : mv_polynomial (option β) α ≃+* polynomial (mv_polynomial β α) :=
id                                          └┘  └┘                                   
src                                         └┘  └┘
typ                                         └┘  └┘                                   
1217  (ring_equiv_of_equiv α $ (equiv.option_equiv_sum_punit β).trans (equiv.sum_comm _ _)).trans $
id                                                         
typ                                                        
1218  (sum_ring_equiv α _ _).trans $
id                   
typ                  
1219  punit_ring_equiv _
1220  
1221  /--
1222  The ring isomorphism between multivariable polynomials in `option β` and
1223  multivariable polynomials with coefficients in polynomials.
1224  -/
1225  def option_equiv_right : mv_polynomial (option β) α ≃+* mv_polynomial β (polynomial α) :=
id                                           └┘  └┘                                   
src                                          └┘  └┘
typ                                          └┘  └┘                                   
1226  (ring_equiv_of_equiv α $ equiv.option_equiv_sum_punit.{0} β).trans $
id                                                            
typ                                                           
1227  (sum_ring_equiv α β unit).trans $
id                     └──┘
src                      └──┘
typ                    └──┘
doc                      └──┘
1228  ring_equiv_congr (mv_polynomial unit α) (punit_ring_equiv α)
id                                   └──┘                     
src                                  └──┘
typ                                  └──┘                     
doc                                  └──┘
1229  
1230  end
1231  
1232  end equiv
1233  
1234  end mv_polynomial